%-----------------------------------------------------------------------------
%
%               Template for sigplanconf LaTeX Class
%
% Name:         sigplanconf-template.tex
%
% Purpose:      A template for sigplanconf.cls, which is a LaTeX 2e class
%               file for SIGPLAN conference proceedings.
%
% Guide:        Refer to "Author's Guide to the ACM SIGPLAN Class,"
%               sigplanconf-guide.pdf
%
% Author:       Paul C. Anagnostopoulos
%               Windfall Software
%               978 371-2316
%               paul@windfall.com
%
% Created:      15 February 2005
%
%-----------------------------------------------------------------------------


\documentclass{llncs}

% The following \documentclass options may be useful:
%
% 10pt          To set in 10-point type instead of 9-point.
% 11pt          To set in 11-point type instead of 9-point.
% authoryear    To obtain author/year citation style instead of numeric.
\usepackage{xcolor} 
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{proof}
\usepackage{hyperref}
\usepackage{caption}
\usepackage{subcaption}
\usepackage{fancybox}
\usepackage{diagrams}
\definecolor{light-gray}{gray}{0.86}
\newcommand{\nil}[0]{\mathsf{nil}} 
\newcommand{\cons}[0]{\mathsf{cons}} 
\newcommand{\vecc}[0]{\mathsf{vec}} 
\newcommand{\suc}[0]{\mathsf{S}} 
\newcommand{\nat}[0]{\mathsf{Nat}} 
\newcommand{\ind}[0]{\mathsf{Ind}} 
\newcommand{\app}[0]{\mathsf{app}} 

\newcommand{\selfstar}[0]{$\mathsf{Selfstar}\ $} 
\newcommand{\self}[0]{\mathbf{S}} 
\newcommand{\fomega}[0]{\mathbf{F}_{\omega}} 
\newcommand{\cc}[0]{\mathbf{CC}} 
\newcommand{\gray}[1]{\colorbox{light-gray}{#1}}
\newcommand{\M}[3]{
\{#1_i \mapsto #2_i\}_{i \in #3}} 
\newcommand{\Mb}[4]{
\{#1_i:#4_i \mapsto #2_i\}_{i \in #3}} 

\newcommand{\bm}[4]{
\{(#1_i:#2_i) \mapsto #3_i\}_{i \in #4}} 
\newcommand{\frank}[1]{\textcolor{blue}{\textbf{[#1 ---Frank]}}}
\newarrowfiller{dasheq} {==}{==}{==}{==}
\newarrow {Mapsto} |--->
\newarrow {Line} -----
\newarrow {Implies} ===={=>}
\newarrow {EImplies} {}{dasheq}{}{dasheq}{=>}
\newarrow {Onto} ----{>>}
\newarrow {DashInto} C{dash}{}{dash}{>}
\newarrow {Dashto}{}{dash}{}{dash}{>}
\newarrow {Dashtoo}{}{dash}{}{dash}{>>}
\begin{document}
%% \conferenceinfo{WXYZ '05}{date, City.} 
%% \copyrightyear{2005} 
%% \copyrightdata{[to be supplied]} 

%% \titlebanner{banner above paper title}        % These are ignored unless
%% \preprintfooter{short description of paper}   % 'preprint' option specified.

\title{Church Encoding with Dependent Types}
%%\subtitle{Extended Abstract}

%% \authorinfo
%%            {Peng Fu}

\author{Peng Fu, Aaron Stump}
\institute{Computer Science, The University of Iowa}


\maketitle

\begin{abstract}
We introduce $\self$, a Curry-style dependent type
system featuring new type assignment rules for the \textit{self type} $\iota x.T$, 
together with restrictive  mutually recursive definitions and Miquel's implicit product $\forall x:T.T'$.
 We show how to obtain Church-encoded datatypes and the corresponding induction principles with $\self$. A notion of erasure from $\self$  to $\fomega$ with let-bindings is defined, thus establishing strongly normalization for the terms. Type preservation is proved by combining several confluence techniques with Barendregt's method for proving subject reduction for Curry-style System \textbf{F}. 
\end{abstract}

%% \category{CR-number}{subcategory}{third-level}

%% \terms
%% term1, term2

%% \keywords
%%  Lambda Encoding, Dependent Type, Type preservaiton, Progress, Confluence

\section{Introduction} 
\label{sec:intro}
%% \section{Lambda Encodings}
It is well known that the natural numbers can be encoded as lambda terms using
Church encoding \cite{Church:1985} or Scott encoding (reported in \cite{CHS:72}).  Thus operations such as \textit{addition}, 
\textit{multiplication} can be performed by beta-reduction
 on lambda terms. Other inductive data structures such as trees and lists (\cite{Barendregt:97}, chapter 11 in \cite{Girard:1989})
can also be represented in a similar fashion. 

Church-encoded data can be represented in System \textbf{F}\cite{Girard:72}, but it is rarely adopted in theorem provers based on dependent types. As summarized in Werner's \cite{Werner:92}, it is ineffecient to define certain operation on Church-encoded data, e.g. the \textit{predecessor} function; the induction principle is not derivable within Calculus of Construction ($\cc$); and  $0 \not = 1$ can not be proved within $\cc$. These problems provide reasons for treating inductive datatypes as primitive \cite{Paulin:1993}. We want to stress that the ineffeciency to retrieve subdata is an inherent problem for Church encoding, $0 \not = 1$ is unprovable in $\cc$ is because the notion of the contradiction is inadequate, and the underivability of induction principle shows the limitation of $\cc$. 

In this paper, we explore another point of view,
namely, adapt $\cc$ to fit Church encoding. The results of our work show that
this point of view is viable and can potentially simplify the design of
dependently typed languages. More specifically, we make the following technical contributions:

\begin{itemize}
\item We propose System $\self$, which allows us to derive induction principles for Church-encoded data. We also propose to change the notion of contradiction, which enables us to derive
  $0 \not = 1$ in System $\self$.
  
\item We prove strong normalization of $\self$ by erasing it to $\fomega$ with let-bindings.
  
  \item We show how to prove type preservation by applying several confluence results and techniques. 
\end{itemize}

%% Scott encoding does not suffer the ineffeciency problem arised in Church encoding. But in order to define recursive functions on Scott numerals, one need either the fixpoint operator or some form of self-application(as reported in \cite{Jansen:2011}). So it seems that Scott numerals can hardly fit into a total intuitionistic type theory. \footnote{Scott numerals was claimed to be typable in System \textbf{F} \cite{Abadi:93}, but we are not sure exactly how that works.}

%% Moreover, even when recursive definition is allowed, it is still unclear how one can derive elimination scheme to define datatype such as vector and vector append function in common dependently typed language. 

%% \frank{I am still not sure in a language with mutual recursion and type:type, what notion of proof we have in mind? } 


\subsection{Induction Principle}
We shall take a closer look at the difficulties of deriving an induction principle for Church
numerals in $\cc$, then offer our solutions. 
In $\cc$ \`a la Curry, let $ \mathsf{Nat} := \Pi X.(X \to X) \to X \to X$. One can obtain a notion of \textit{indexed iterator} by $\mathsf{It} := \lambda x.\lambda f.\lambda a. x f a$ and $\mathsf{It}: \Pi X.\Pi x:\mathsf{Nat}. (X \to X) \to X \to X$. Thus we have 
 $\mathsf{It}\ \bar{n} =_{\beta} \lambda f.\lambda a. \bar{n}\ f\ a =_{\beta}\lambda f.\lambda a. \underbrace{f ( f ( f...(f}_{n} a)...))$. 
 One may want to know if we can obtain a finer version, namely, the induction principle-$\mathsf{Ind}$ such that:

$\mathsf{Ind} :\Pi P:\mathsf{Nat} \to *. \Pi x:\mathsf{Nat}. (\Pi y:\mathsf{Nat}.(P y \to P(\mathsf{S} y))) \to P\ \bar{0} \to P\ x$ 

\noindent Let us try to construct such $\mathsf{Ind}$. First observe the following beta-equalities and typings:


$\mathsf{Ind} \ \bar{0} =_{\beta} \lambda f.\lambda a.a $

$\mathsf{Ind} \ \bar{0} : (\Pi y:\mathsf{Nat}.(P y \to P(\mathsf{S} y))) \to P\ \bar{0} \to P\ \bar{0}$

$\mathsf{Ind} \ \bar{n} =_{\beta} \lambda f.\lambda a.\underbrace{f\ \overline{n-1} (... f\ \bar{1}\ (f}_{n>0}\ \bar{0}\ a)) $

$\mathsf{Ind} \ \bar{n} : (\Pi y:\mathsf{Nat}.(P y \to P(\mathsf{S} y))) \to P\ \bar{0} \to P\ \bar{n}$


with $f:\Pi y:\mathsf{Nat}.(P y \to P(\mathsf{S} y)), a: P\ \bar{0}$

\noindent The equalities above suggest that $\mathsf{Ind} := \lambda x.\lambda f.\lambda a.x\ f\ a$, 
with a different notion of lambda numerals, i.e. 

$\bar{0}:= \lambda s.\lambda z.z$

$\bar{n}:= \lambda s.\lambda z.s\ \overline{n-1}\ (\overline{n-1}\ s\ z)$ 

\noindent %% We want to remark that this notion of lambda numerals have been discovered independently by many others(cite).
Each numeral corresponds to its terminating recursion. They are not exactly Church numerals because each numeral contains its subdata., similarly to Scott numerals.  

Now, let us try to type these 
lambda numerals. It is reasonable to assign $s:\Pi y:\mathsf{Nat}.(P\ y \to P(\mathsf{S}\ y))$
and $z: P\ \bar{0}$. Thus we have the following typing relations: 

$\bar{0} : \Pi y:\mathsf{Nat}.(P\ y \to P(\mathsf{S}\ y)) \to P\ \bar{0} \to P\ \bar{0}$

$\bar{1} : \Pi y:\mathsf{Nat}.(P\ y \to P(\mathsf{S}\ y)) \to P\ \bar{0} \to P\ \bar{1}$

$\bar{n} : \Pi y:\mathsf{Nat}.(P\ y \to P(\mathsf{S}\ y)) \to P\ \bar{0} \to P\ \bar{n}$

\noindent So we have the following definition:

$\mathsf{Nat} := \Pi P: \mathsf{Nat}\to *.\Pi y:\mathsf{Nat}.(P\ y \to P(\mathsf{S}\ y)) \to P\ \bar{0} \to P\ \bar{n}$ for any $\bar{n}$. 

\noindent Two problems arise with this scheme of encoding. The first problem involves mutually recursiveness. The definiens of $\mathsf{Nat}$ contains $\mathsf{Nat}$ and $\mathsf{S}, \bar{0}$, while the type of $\mathsf{S}$ is $\mathsf{Nat} \to \mathsf{Nat}$ and the type of $\bar{0}$ is $\mathsf{Nat}$. So the typing of $\mathsf{Nat}$ will be mutually recursive. Observe that the recursive occurrences of $\mathsf{Nat}$ are all at the type-annotated positions; i.e., the right side of the ``$:$''. 

Note that the subdata of $\bar{n}$ is responsible for one recursive occurrence of $\mathsf{Nat}$, namely, $\Pi y:\mathsf{Nat}$. If one never computes with the subdata, then these numerals will behave just like Church numerals. This inspires us to use Miquel's implicit product \cite{miquel:2001}. So we redefine $\mathsf{Nat}$ to be:

$\mathsf{Nat} := \Pi P: \mathsf{Nat}\to *.\forall y:\mathsf{Nat}.(P\ y \to P(\mathsf{S}\ y)) \to P\ \bar{0} \to P\ \bar{n}$ for any $\bar{n}$. 

\noindent Here $\forall y:\mathsf{Nat}$ is the implicit product. Now our notion of numerals are exactly Church numerals instead of Scott's derivative. Even better, this definition of $\mathsf{Nat}$ can be erased meaningfully to $\fomega$. $\fomega$'s types do not have dependency on terms, so $P:\mathsf{Nat} \to *$ will get erased to $P:*$ and it is known that one can also erase the implicit product\cite{ahn:2013}. The erasure of $\mathsf{Nat}$ will be $\Pi P:  *.(P \to P) \to P \to P$, which is the definition of $\mathsf{Nat}$ in $\fomega$. As long as 
we restrict the recursive occurrences of the type to be at the erased positions, we will have a meaningful interpretation over $\fomega$. 

The second problem is about quantification. We want to define a type $\mathsf{Nat}$ for any $\bar{n}$, but right now what we really have is one $\mathsf{Nat}$ for each numerals $\bar{n}$. 
 We solve this problem by introducing a new type construct $\iota x.T$ called \textit{self type}. Thus we define

$\mathsf{Nat} := \iota x.\Pi P:\mathsf{Nat} \to *.\forall y:\mathsf{Nat}.(P\ y \to P(\mathsf{S}\ y)) \to P\ \bar{0} \to P\ x$

\noindent We require that the self type can only be instantiated/generalized by its own subject, so we add the following two rules:
\[
\begin{array}{cc}
  \infer[\textit{selfGen}]{\Gamma \vdash t: \iota x.T}{\Gamma \vdash t: [t/x]T}
&
 \infer[\textit{selfInst}]{\Gamma \vdash t: [t/x]T}{\Gamma \vdash t: \iota x.T}
\\
\end{array}
\]

\noindent We have the following inference\footnote{The double bar means that the converse of the inference rule is also true.}:
\[
\begin{array}{c}
\infer={\bar{n}: \iota x.\Pi P:\mathsf{Nat} \to *.\forall y:\mathsf{Nat}.(P\ y \to P(\mathsf{S}\ y)) \to P\ \bar{0} \to P\ x}{\bar{n} : \Pi P:\mathsf{Nat} \to *.\forall y:\mathsf{Nat}.(P\ y \to P(\mathsf{S}\ y)) \to P\ \bar{0} \to P\ \bar{n}} 
\end{array}
\]

\subsection{The Notion of Contradiction}

In $\cc$ \`a la Curry, it is customary to use $\Pi X:*.X$ as the notion of contradiction, since an inhabitant of the type $\Pi X:*.X$ will inhabit any type, so the law of explosion is subsumed by the type $\Pi X:*.X$. However, this notion of contradiction is too strong to be useful. Let $t =_A t'$ denote $\Pi C: A \to *. C t \to C t'$ with $A:*, t:A, t':A$. Then $0 =_{\nat} 1$ can be expanded to $\Pi C:\nat \to *. C 0 \to C 1$ ($0$ is Leibniz equals to $1$). One can not derive a proof for $(\Pi C:\nat \to *. C 0 \to C 1) \to \Pi X:*.X$, because the erasure of $(\Pi C:\nat \to *. C 0 \to C 1) \to \Pi X:*.X$ in System \textbf{F} would be $(\Pi C:*. C \to C) \to \Pi X:*.X$, and we know that $\Pi C:*. C \to C$ is inhabited. So the inhabitation of $(\Pi C:\nat \to *. C 0 \to C 1) \to \Pi X:*.X$ will imply the inhabitation of $\Pi X:*.X$. If we take Leibniz equality, then using $\Pi X:*.X$ as the notion of contradiction is so strong that we simply can not prove any negative results about equality. 

On the other hand, an equational theory is considered inconsistent if $a = b$ for all term $a$ and $b$. This motivates us to use this as the notion of contradiction. We propose to use $\Pi A:*.\Pi x:A.\Pi y:A. x =_A y$ as the notion of contradiction in $\cc$. We first want to make sure it is uninhabited. The way to argue that is first assume it is inhabited by $t$. Since $\cc$ is strongly normalizing, the normal form of $t$ must be of the form\footnote{We use square [ ] to mean the type inside is only for typing.} $[\lambda A:*.]\lambda x[:A].\lambda y[:A].[\lambda C:A \to *].\lambda z[: C\ x]. n$ for some normal term $n$ with type $C\ y$, but we know that there is no combination of $x,y,z$ to make a term of type $C\ y$. So the type $\Pi A:*. \Pi x:A.\Pi y:A. \Pi C: A \to *. C x \to C y$ is uninhabited. Then, we want to make sure this notion of contradiction is usable, namely, we want to prove the following theorem.  

\begin{theorem}
  \label{contract}
  $0 = 1 \to \bot$ is inhabited in $\cc$, where $\bot := \Pi A:*.\Pi x:A.\Pi y:A. \Pi C: A \to *. C x \to C y$, $0 := \lambda s.\lambda z.z$, $1 := \lambda s.\lambda z.s\ z$.
\end{theorem}
\begin{proof}
  Assume $\nat := \Pi B:*. (B \to B) \to B\to B$. Let $\Gamma = a : (\Pi D: \nat \to *. D 0 \to D 1), A:*, x:A, y:A, C:A \to *, c: C\ x$. We want to construct a term of type $C\ y$. Let $F := \lambda n[:\nat]. n\ [A]\ (\lambda q[:A].y) x$. Note that 
  $F: \nat \to A$. We know that
 $F 0 =_{\beta} x$ and $F 1 =_{\beta} y$. So we can indeed convert the type of $c$ from $C x$ to $C\ (F 0)$. And then we instantiate the $D$ in $\Pi D: \nat \to *. D 0 \to D 1$ with $\lambda x[:\nat].C\ (F x)$. So we have $C\ (F 0) \to C\ (F 1)$ as the type of $a$. So $a c : C (F 1)$, which means $a c : C y$. So we just show how to inhabit $0 = 1 \to \bot$ in $\cc$\footnote{The Coq code for this example is in appendix \ref{coq}}. 
  
\end{proof}

Once $\bot$ is derived, one can not distinguish the domain of individuals. Note that this notion of contradiction does not admit law of explosion.  

\subsection{Overview}

%% In this talk, we will motivate the \selfstar by the consideration of induction principle, and
%% then we will go over some of the important typing rules for \selfstar. Finally, we will see how standard Church- and Scott-encoded datatype can be presented in \selfstar system.

%% as terms in \selfstar, with corresponding induction and case analysis schemes.

%% We have glimpsed that induction principle can be recovered in \selfstar at the present of 
%% self type, mutual recursive definitions. We also add $*:*$ for type-level computation and excluding the needs for multi-level data type.
%% This is make \selfstar a powerful and yet somewhat simple as a full fledged dependent typed
%% programming language.


%% The present of mutual recursive definitions and $*:*$ are more than enough to depart from
%% the Curry-Howard correspondence. We want to argue that recursive definitions 
%% are there only for defining datatype like $\mathsf{Nat}$. If we 
%% want a total type theory, we can abandon $*:*$ and erase the system to $\mathbf{F}_{\omega}$, 
%% thus normalization is concluded. 



In section \ref{self}, we present a novel type System $\self$, which not only enables us to type Church-encoded data, but also allows us to derive the corresponding induction principles. Several examples about numerals and vectors are given to demonstrate the power of $\self$. 

 %% \selfstar itself is inconsistent from the formula-as-type point of view, due to the presents of mutual recursive definitions and $*:*$. But with these two features, together with Scott encoded data, we use several examples to demonstrate that \selfstar can serve as a powerful dependent typed programming langauge. 

In section \ref{s}, we show how to erase $\self$ to $\fomega$, thus established the consistency of $\self$. Type preservation of $\self$ is proved by applying several techniques: Hardin's interpretation method\cite{Hardin:1989}, Hindley-Rosen's commutativity method\cite{hindley1964}\cite{Rosen:1973}, typing as rewrite relation (inspired by \cite{kuan2007}\cite{stump2011}) and Barendregt's method of proving subject reduction for Curry-style System \textbf{F}\cite{barendregt:1993} . The difficulties arise when we try to handle mutually recursive definitions, together with several non-syntax-directed rules. Although the proof method we developed is specific for our system, we believe that it can be adapted to prove type preservation for other Curry-style systems that make use of mutually recurisve definitions. Finally, we give a proof of $0 \not = 1$ in $\self$ in section \ref{zero}, following the approach of the proof of Theorem \ref{contract}. 
%% Definitions of abstract reduction system, lambda calculus, simple types are given in section \ref{Pre}. We present Scott and Church numerals in both untype and typed forms in section \ref{Types}. Dependent type system and the related problem with Church encoding are discussed in detail in section \ref{Dep}. Seciton \ref{Conf}, several methods to show \textit{confluence} are given. We give an outline of proving confluence for the term system of $\mathsf{Selfstar}$ (Section \ref{Local}). Relation of confluence to type preservation is discussed in Section \ref{Conf:Presv}.  We present system $\mathsf{Selfstar}$ (Section \ref{Self}), which not only enable us to type Scott encoding and Church encoding data, but also allow us to derive corresponding induction principle and case analysis principle. 

\section{Church Encoding in $\self$}
\label{self}
%\frank{need to add a paragraph here}
There are two differences between $\self$ and $\cc$: the first one is the self 
type, and the second one is the recursive definitions. Intuitively, it seems impossible to obtain a consistent system while allowing recursive definitions. To maintain a well-defined erasure over $\fomega$, we restrict the following: there is no recursive definition at term level and the recursive occurrences of type can only be at the erased positions at type level. If we take consistency in the sense that not every type is inhabited, then the well-defineness of the erasure will imply that the type $\Pi X:*.X$ in $\self$ will not be inhabited, resulting the consistency of $\self$. Self types provide a mechanism for the type to refer to its subject. With these two features, we gain the ability to quantify over the subject in $\self$, which is missing in $\cc$.  

\subsection{System $\self$}
We use gray boxes to highlight the terms, types and rules that are not in $\fomega$ with let-bindings. We also include a full specification of $\fomega$ with let-bindings in appendix \ref{fomega}. 
%In order to avoid the overuse of $\Pi$, we use $\xi$ and $\zeta$ as the kind-level binders.
\begin{definition}[Syntax]
\

\footnotesize{

\noindent \textit{Terms} $t \ :: = \ x \ | \ \lambda x.t \ | \ t t' \ | \ \mu t$

\noindent \textit{Types} $T \ ::= $

\noindent $\ X \ | \ \Pi X:\kappa.T \ | \ \Pi x:T_1.T_2 \ | \ \gray{$\forall x:T_1.T_2$} \ | \ \gray{$\iota x.T$} \ | \ \gray{$T \ t$} \ | \ \lambda X.T \ | \ \gray{$\lambda x.T$}\ | \ T_1 T_2 \ | \ \mu T$

\noindent \textit{Kinds} $\kappa \ ::= \ * \ | \ \gray{$\Pi x:T.\kappa$} \ | \  \Pi X:\kappa'. \kappa \  | \ \gray{$\mu \kappa$}$ 

\noindent \textit{Context} $\Gamma \ :: = \ \cdot \ | \ \Gamma, x:T \ |  \ \Gamma, X:\kappa\ | \ \Gamma, \tilde{\mu}$

\noindent \textit{Closure} $\mu \ ::= \ \M{x}{t}{N} \cup \M{X}{T}{M}$
}
\end{definition} 
\noindent \textbf{Remarks} :

\begin{itemize}
  \item For $\M{x}{t}{N}$, we do not allow any recursive (or mutually recursive) definitions, so they are let-bindings. For $\M{X}{T}{M}$, we do not allow mutually recursive type definitions, and the recursive occurrence of type can only be at the erased positions, namely, only at the right side of ``$:$'' under the binder $\Pi$ and $\forall$. 
  \item If $\mu$ is $\M{x}{t}{N}\cup \M{X}{T}{M}$, then $\tilde{\mu}$ is $\bm{x}{T}{t}{N} \cup \bm{X}{\kappa}{T}{N}$ for some type $T_i$, kind $\kappa_i$.

    \item   For $\M{x}{t}{N}\cup \M{X}{T}{M}$, we
require for any $ 1 \leq i \leq n $, the free variable set $\mathrm{FV}(t_i) = \emptyset$ and for any $ 1 \leq i \leq m $, the free term and type variable of $T_i$, $\mathrm{FV}(T_i) \subseteq \mathrm{dom}(\mu)$ . We also do not allow any reductions and substitutions inside the closure. We call this the \textit{locality} restriction.
%% and each $t_i$ is \textit{pure}(i.e. does not contain any closure),  we call this requirement \textit{local property}. The motivation of purity requirement come from the following intuition: when ever $\mu_1, \Gamma_1, \{ x \mapsto \mu_1 y\}$, then we can reformulate it
%% as $\Gamma_1, \mu_1 \cup \{ x \mapsto y\}$. Purity is used in the proof of lemma \ref{erase:eq}.
Locality is a very important property that will be assumed or used through out this paper.  On the other hand, without locality requirement, we predict it is impossible to establish confluence (see \cite{Ariola:1997}). 

%% \item $\vec{\mu}t$ denotes $\mu_1...\mu_n t$. $\vec{\mu}$ here and through out this article is not allowed to be an empty closure. We do have a notation for allowing possibly empty many closure, namely, $\dot{\vec{\mu}}$. 

\item $\mathrm{FV}(\mu t) = \mathrm{FV}(t) - \mathrm{dom}(\mu)$, same for $\mu T, \mu \kappa$. 

%% $[t'/x](\mu t )\ \equiv \mu([t'/x]t)$ and
%% $[t'/x](\iota y.t )\ \equiv \iota y. [t'/x]t$.
\end{itemize}

\begin{figure}
\begin{center}
\begin{tabular}{lll}
\infer{ \cdot \vdash \mathsf{wf}}{}

&

&
\infer{ \Gamma, x:T \vdash \mathsf{wf}}{\Gamma \vdash \mathsf{wf} & \Gamma \vdash T:*}

\\
\\

\infer{ \Gamma, X:\kappa \vdash \mathsf{wf}}{\Gamma \vdash \mathsf{wf} & \Gamma \vdash \kappa:\Box}
&

&
\infer{\Gamma, \tilde{\mu} \vdash \mathsf{wf}}{\Gamma \vdash \mathsf{wf}
& \Gamma, \tilde{\mu} \vdash \mathsf{ok}}
\end{tabular}
\end{center}
\caption{Well-formed Context \fbox{$\Gamma \vdash \mathsf{wf}$}}
\label{fig:sub1}
\end{figure}

\begin{figure}
\begin{center}
\begin{tabular}{ll}

\infer{\Gamma \vdash *:\Box}{}

&

\infer{\Gamma \vdash \Pi X:\kappa'.\kappa: \Box}{\Gamma, X:\kappa' \vdash \kappa : \Box & 
\Gamma  \vdash \kappa' : \Box}

\\
\\

\gray{\infer{\Gamma \vdash \Pi x:T.\kappa: \Box}{\Gamma, x:T \vdash \kappa : \Box
& \Gamma \vdash T:*}}

&

\infer{\Gamma \vdash \mu \kappa:  \Box}{\Gamma, \tilde{\mu}
\vdash \kappa:\Box & \Gamma, \tilde{\mu} \vdash \mathsf{ok}}
\end{tabular}
\end{center}
\caption{Well-formed Kind \fbox{$\Gamma \vdash \kappa : \Box$}}
\label{fig:sub2}
\end{figure}

\begin{figure}
\begin{center}
\footnotesize{
\begin{tabular}{ll}
\infer{\Gamma \vdash X:\kappa}{(X:\kappa) \in \Gamma}

&
\infer{\Gamma \vdash T : \kappa'}{\Gamma \vdash T:
\kappa & \Gamma \vdash \kappa \cong \kappa' & \Gamma \vdash \kappa': \Box}

\\
\\
\infer{\Gamma \vdash \Pi x:T_1.T_2 : *}{ \Gamma \vdash T_1 : * &
\Gamma, x: T_1 \vdash T_2 : *}

&


\infer{\Gamma \vdash \Pi X:\kappa. T : *}{ \Gamma, X:\kappa \vdash T : * & \Gamma \vdash \kappa:\Box}

\\
\\

\infer{\Gamma \vdash \mu T: \mu \kappa}{\Gamma, \tilde{\mu}
\vdash T:\kappa & \Gamma, \tilde{\mu} \vdash \mathsf{ok}}

&

\gray{\infer[\textit{Self}]{\Gamma \vdash \iota x.T : *}{\Gamma, x:\iota x.T \vdash T : *}}
\\
\\

\infer{\Gamma \vdash \lambda X.T: \Pi X:\kappa. \kappa'}{\Gamma, X:\kappa \vdash T : \kappa' & \Gamma \vdash \kappa : \Box }

&
\gray{
\infer{\Gamma \vdash \lambda x.T: \Pi x:T'.\kappa}{\Gamma, x:T' \vdash T : \kappa & \Gamma \vdash T':*}
}
\\
\\
\gray{\infer{\Gamma \vdash S t: [t/x]\kappa}{\Gamma \vdash S: \Pi x:T.\kappa & 
\Gamma \vdash t:T}}

&

\infer{\Gamma \vdash S T: [T/X]\kappa}{\Gamma \vdash S: \Pi X:\kappa'.\kappa & 
\Gamma \vdash T:\kappa'}

\\
\\
\gray{
\infer{\Gamma \vdash \forall x:T_1.T_2 : *}{ \Gamma, x:T_1 \vdash T_2 : * &
\Gamma \vdash T_1 : *}
}
\end{tabular}
}

\end{center}
      \caption{Kinding \fbox{$\Gamma \vdash T : \kappa$}}      
    \end{figure}

    \begin{figure}
\begin{center}
\footnotesize{
\begin{tabular}{ll}

\infer[\textit{Conv}]{\Gamma \vdash t : T_2}{\Gamma \vdash t:
T_1 & \Gamma \vdash T_1 \cong T_2 & \Gamma \vdash T_2:*}
&
\infer[\textit{Var}]{\Gamma \vdash x:T}{(x:T) \in \Gamma}

\\

\\
\gray{
\infer[\textit{SelfGen}]{\Gamma \vdash t : \iota x.T}{\Gamma
\vdash t: [t/x]T & \Gamma \vdash \iota x.T: *}
}
&

\gray{
\infer[\textit{SelfInst}]{\Gamma \vdash t: [t/x]T}{\Gamma
\vdash t : \iota x.T}
}
\\
\\
\gray{
\infer[\textit{Indx}]{\Gamma \vdash t : \forall x:T_1.T_2}
{\Gamma, x:T_1 \vdash t: T_2 & \Gamma \vdash T_1:* & x \notin \mathrm{FV}(t)}
}
&
\gray{
\infer[\textit{Dex}]{\Gamma \vdash t :[t'/x]T_2}{\Gamma
\vdash t: \forall x:T_1.T_2 & \Gamma \vdash t': T_1}
}
\\
\\

\infer[\textit{Mu}]{\Gamma \vdash {\mu} t: \mu T}{\Gamma, \tilde{\mu}
\vdash t:T &  \Gamma, \tilde{\mu} \vdash \mathsf{ok}}
&

\infer[\textit{Poly}]{\Gamma \vdash  t :\Pi X:\kappa.T}
{\Gamma, X:\kappa \vdash t: T & \Gamma \vdash \kappa:\Box}

\\
\\
\infer[\textit{Inst}]{\Gamma \vdash t:[T'/X]T}{\Gamma \vdash t: \Pi X:\kappa.T 
& \Gamma \vdash T': \kappa}

&

\infer[\textit{Func}]{\Gamma \vdash \lambda x.t : \Pi x:T_1. T_2}
{\Gamma, x:T_1 \vdash t: T_2 & \Gamma \vdash T_1:*}

\\
\\
\infer[\textit{App}]{\Gamma \vdash t t':[t'/x]T_2}{\Gamma
\vdash t: \Pi x:T_1. T_2 & \Gamma \vdash t': T_1}

\end{tabular}
}
\end{center}
      
      \caption{Typing \fbox{$\Gamma \vdash t : T$}}
      
    \end{figure}

\newpage
\noindent \textbf{Remarks} :

\begin{itemize}
 \item $\Gamma, \tilde{\mu} \vdash \mathsf{ok}$ stands for $\{\Gamma, \tilde{\mu} \vdash t_j: T_j\}_{(t_j:T_j) \in \tilde{\mu}}$ and $\{\Gamma, \tilde{\mu} \vdash T_j: \kappa_j\}_{(T_j:\kappa_j) \in \tilde{\mu}}$.
  
\item $(t_i : T_i) \in \tilde{\mu}$ means $(x_i:T_i) \mapsto t_i \in \tilde{\mu}$ and $(T_i : \kappa_i) \in \tilde{\mu}$ means $(X_i:\kappa_i) \mapsto T_i \in \tilde{\mu}$. 
 \item $\cong $ is the reflexive transitive and symmetry closure of $\to_{\beta} \cup \to_o \cup \to_{\mu}$. 
 
\item Typing and kinding do not depend on well-formness of the context, so the self type formation rule \textit{self} is not circular in this sense. %% In fact, we can even show: if $\Gamma \vdash \mathsf{wf}$ and $\Gamma \vdash t:t'$, then $\Gamma \vdash t':*$(see appendix).


\end{itemize}



\begin{figure}
\centering
\footnotesize
\begin{tabular}{lll}

\infer{\Gamma \vdash\mu x_i \to_{\beta} \mu t_i}{(x_i \mapsto
t_i) \in \mu}

&
\infer{\Gamma \vdash x \to_{\beta} t}{(x\mapsto t) \in \Gamma}

&
\infer{\Gamma \vdash(\lambda x.t)t' \to_{\beta} [t'/x]t}{}

\\
\\
\infer{\Gamma \vdash\mu X_i \to_{\beta} \mu T_i}{(X_i \mapsto
T_i) \in \mu}



&
\infer{\Gamma \vdash X \to_{\beta} T}{(X\mapsto T) \in \Gamma}
&
\gray{
\infer{\Gamma \vdash(\lambda x.T)t \to_{\beta} [t/x]T}{}
}
\\
\\

\infer{\Gamma \vdash(\lambda X.T)T' \to_{\beta} [T'/X]T}{}


\end{tabular}
\caption{Beta Reduction}
\end{figure}  


\begin{figure}
\centering
  \footnotesize{
\begin{tabular}{ll}

\infer{\Gamma \vdash \mu t \to_{o} t}{\mu \in \Gamma}

&

\infer{\Gamma \vdash \mu T \to_{o} T}{\mu \in \Gamma}

\\
\\
\infer{ \Gamma \vdash \mu t \to_{\mu} t}{\mathrm{dom}(\mu) \#
\mathrm{FV}(t)}

&
\infer{ \Gamma \vdash \mu(\lambda x.t) \to_{\mu} \lambda x.\mu
t}{}

\\
\\

\infer{ \Gamma \vdash \mu(t_1 t_2)  \to_{\mu} (\mu t_1 ) (\mu
t_2)}{}

&

\infer{ \Gamma \vdash \mu(T\ T') \to_{\mu} (\mu T)(\mu T')}{}

\\
\\

\infer{ \Gamma \vdash \mu T \to_{\mu} T}{\mathrm{dom}(\mu) \#
\mathrm{FV}(T)}

&
\gray{
\infer{ \Gamma \vdash \mu(\iota x.T) \to_{\mu} \iota x.\mu T}{}
}
\\
\\

\gray{
\infer{ \Gamma \vdash \mu(\forall x:T_1.T_2) \to_{\mu} \forall x:\mu T_1.\mu T_2}{}
}
&

\infer{ \Gamma \vdash \mu(\Pi X:\kappa.T) \to_{\mu} \Pi X:\mu \kappa.\mu T}{}

\\
\\

\gray{
\infer{ \Gamma \vdash \mu(T\ t) \to_{\mu} (\mu T)(\mu t)}{}
}
&

\infer{ \Gamma \vdash \mu(\lambda X.T) \to_{\mu} \lambda X.\mu T}{}

\\
\\

\gray{
\infer{ \Gamma \vdash \mu(\lambda x.T) \to_{\mu} \lambda x.\mu T}{}
}
&
\infer{ \Gamma \vdash \mu(\Pi x:T_1.T_2) \to_{\mu} \Pi x:\mu
T_1.\mu T_2}{}


\end{tabular}
}  

  \caption{O reduction and Mu Reduction}
  
\end{figure}


\newpage
\noindent \textbf{Remarks}:

\begin{itemize}
\item $x_i \mapsto t_i \in \tilde{\mu}$ means $(x_i:T_i) \mapsto t_i \in \tilde{\mu}$ for some $T_i$ and $X_i \mapsto T_i \in \tilde{\mu}$ means $(X_i:\kappa_i) \mapsto T_i \in \tilde{\mu}$ for some $\kappa_i$. 
\item We list only the essential reduction rules for terms and types. For the whole specification of reductions, see appendix \ref{fullred}.

\item One can see that beside beta-reduction, we have mu-reduction to move the closure inside the term or type structure.

\item At the type level, we want to discard a closure when it is already in the context. o-reduction allow us to do this. Without this type level reduction, we can not prove the type
preservation theorem. Note that we do not allow o-reduction at term level.

\end{itemize}


\subsection{Church Encoding in $\self$}
Now let us see some concrete examples of Church encodings in $\self$. For convenience, we write $T \to T'$ for $\Pi x:T.T'$ with $x \notin \mathrm{FV}(T')$.

\begin{definition}[Church Numerals]
Let $\tilde{\mu}_c$ be the following recursive defintions:

\noindent $(\mathsf{Nat}:* ) \mapsto \iota x. \Pi C: (\Pi y:\mathsf{Nat}. *).  (\forall n : \mathsf{Nat}. (C\ n) \to (C\ (\mathsf{S}\ n))) \to (C\ 0) \to (C\ x)$

\noindent $(\mathsf{S}: \mathsf{Nat} \to \mathsf{Nat} )\mapsto \lambda n.\lambda s.\lambda z. s \ (n\ s\ z)$

\noindent $(0:\mathsf{Nat})  \mapsto  \lambda s. \lambda z.z$
\end{definition}

\noindent With $s: \forall n : \mathsf{Nat}. (C\ n) \to (C\ (\mathsf{S}\ n)), z: C 0, n: \mathsf{Nat}$, we have $\tilde{\mu}_c \vdash \mathsf{wf}$ (using \textit{selfGen} and \textit{selfInst} rules). Also note
that the $\tilde{\mu}_c$ satisfies the constraints on recursive definitions. 

\begin{theorem}[Induction Principle]
\

\noindent $\tilde{\mu}_c \vdash \mathsf{Ind} : \Pi C: (\Pi y:\mathsf{Nat}. *). (\forall n : \mathsf{Nat}. (C\ n) \to (C\ (\mathsf{S}\ n))) \to C\ 0 \to \Pi n:\mathsf{Nat}. C\ n$  

\noindent where $\mathsf{Ind}\ := \lambda s.\lambda z. \lambda n. n\ s\ z$

\noindent with $s:\forall n : \mathsf{Nat}. (C\ n) \to (C\ (\mathsf{S}\ n)), z: C 0, n : \mathsf{Nat}$.
\end{theorem}
\begin{proof}
  Let $\Gamma = \tilde{\mu}_c, C: (\Pi y:\mathsf{Nat}. *), s:\forall n : \mathsf{Nat}. (C\ n) \to (C\ (\mathsf{S}\ n)), z: C 0, n : \mathsf{Nat}$. Since $n : \mathsf{Nat}$, by \textit{selfInst}, $n : \Pi C: (\Pi y:\mathsf{Nat}. *).  (\forall y : \mathsf{Nat}. (C\ y) \to (C\ (\mathsf{S}\ y))) \to (C\ 0) \to (C\ n)$. Thus $n \ s\ z : C\ n$.
\end{proof}
\noindent It is worth noting that it is really the definition of $\mathsf{Nat}$ and the \textit{selfInst} rule that give us the induction principle. We also want to emphasize that this is not 
derivable in $\cc$ \cite{coquand:inria-00075471}. 
\begin{definition}[Addition]
  $ m+n := \mathsf{Ind}\ \suc\ n\ m$
\end{definition}
\noindent One can check that $\tilde{\mu}_c \vdash + : \nat \to \nat \to \nat$ by instantiating the $C$ in the type of $\ind$ by $\lambda y.\nat$, then the type of $\ind$ is $(\nat \to \nat) \to \nat \to (\nat \to \nat)$. 
\begin{definition}[Leibniz's Equality]
 $  \mathsf{Eq}  :=  \lambda A[:*]. \lambda x[:A].\lambda y[:A]. \Pi C: (\Pi y:A.*). C x \to C y$.
\end{definition}
Note that we use $x =_A y$ to denote $\mathsf{Eq}\ A \ x \ y$. We often write $t = t'$ when the type is clear. One can check that if $\vdash A:*$ and $\vdash x, y : A$, then $\vdash x =_A y : *$. 

\begin{theorem}
\noindent $\tilde{\mu}_c \vdash \Pi x : \mathsf{Nat}. x + 0 =_{\nat} x$
\end{theorem}
\begin{proof}
  We prove this by induction. We instantiate $C$ in the type of $\ind$ with $\lambda n. (n + 0) =_{\nat} n$. So by beta reduction at type level, we have $(\forall n : \mathsf{Nat}. ( n + 0 =_{\nat} n) \to ( (\mathsf{S}\ n) + 0 =_{\nat} \suc\ n)) \to  0+0 =_{\nat} 0 \to \Pi n:\mathsf{Nat}. n +0=_{\nat} n$. So for base case, we need to show $0+0 =_{\nat} 0$, which is easy. For step case, we assume $ n + 0 =_{\nat} n$ (Induction Hypothesis), and want to show $(\mathsf{S}\ n) + 0 =_{\nat} \suc\ n$. Since $(\mathsf{S}\ n) + 0 \to_{\beta} \suc\ (n \ \suc \ 0) =_{\beta} \suc (n+0)$,  by congruence on the induction hypothesis, we have $(\mathsf{S}\ n) + 0 =_{\nat} \suc\ n$. Thus $\Pi x : \mathsf{Nat}. x + 0 =_{\nat} x$.
\end{proof}

The proof above is carrying out inside $\self$. It shows how to inhabit the type $\Pi x : \mathsf{Nat}. x + 0 =_{\nat} x$ given $\tilde{\mu}_c$, using $\mathsf{Ind}$. 

For the following vector examples, we use $\vecc(U, n)$ as a meta-level notation for a vector type of length $n$ and the elements in the vector are of type $U$. 

\begin{definition}[Vector]
Let $\tilde{\mu}_v$ be the following recursive definitions:

\noindent  $(\mathsf{vec}(U, n) : *) \mapsto$

$\gray{$\iota x$}. \Pi C: \gray{$(\Pi p:\nat.\Pi q: \vecc(U, p). *)$}.$

$(\Pi m: \mathsf{Nat}.\Pi u:U.\forall y: \vecc(U,m).(  C \  m \ y \  \to C \ (\mathsf{S}m)\ (\mathsf{cons}\ m\ u\ y)))$

$\to C \ 0 \ \mathsf{nil} \to  C\ n\ \gray{$x$}$

\noindent $(\nil:\vecc(U, 0)) \mapsto \lambda y. \lambda x.x$

\noindent $(\cons: \Pi n: \mathsf{Nat}.U \to \vecc (U, n) \to \vecc (U, \suc n)) \mapsto \lambda n.\lambda v. \lambda l. \lambda y. \lambda x.y \ n\ v\ (l \ y\ x)$

\noindent where $n: \mathsf{Nat}, v: U, l: \vecc (U, n), y:\Pi m: \mathsf{Nat}.\Pi u:U.\forall y: \vecc(U,m).(  C \  m \ y \  \to C \ (\mathsf{S}m)\ (\mathsf{cons}\ m\ u\ y)) , x:  C \ 0 \ \nil $. 

\end{definition}

\noindent \textbf{Typing}: It is easy to see that $\nil$ is typable to $\vecc (U, 0)$. Now we show how $\cons$ is typable to $\Pi n: \mathsf{Nat}.U \to \vecc (U, n) \to \vecc (U, \suc n)$. We can see that $l\ y\ x: C\ n\ l$. After the instantiation with $l$, the type of $y \ n\ v$ is $C\ n\ l \to  C\ (\mathsf{S}n)\ (\mathsf{cons}\ n\ v\ l)$. So $y\ n\ v \ (l\ y\ x):  C\ (\mathsf{S}n)\ (\mathsf{cons}\ n\ v\ l)$. So $\gray{$\lambda y. \lambda x. y\ n\ v \ (l\ y\ x)$} :  \Pi C: (\Pi p:\nat.\Pi q: \vecc(U, p). *).(\Pi m: \mathsf{Nat}.\Pi u:U.\forall y: \vecc(U,m).(  C \  m \ y \  \to C \ (\mathsf{S}m)\ (\mathsf{cons}\ m\ u\ y)))\to   C\ 0\ \nil \to C\ (\suc n) \ \gray{$(\lambda y. \lambda x. y\ n\ v \ (l\ y\ x))$} $. So by \textit{selfGen}, we have $\lambda y. \lambda x. y\ n\ v \ (l\ y\ x) : \vecc (U, \suc n)$. Thus $ \cons : \Pi n:\mathsf{Nat}. U \to \vecc(U, n) \to \vecc(U, \suc n)$.
  


\begin{definition}[Induction Principle for Vector]

  \noindent  $\tilde{\mu}_v \vdash \mathsf{Ind}(U, n) : $
  
  $ \Pi C: (\Pi p:\nat.\Pi q: \vecc(U, p). *).$
  
 $(\Pi m: \mathsf{Nat}.\Pi u:U.\forall y: \vecc(U,m).(  C \  m \ y \  \to C \ (\mathsf{S}m)\ (\mathsf{cons}\ m\ u\ y))) $
  
  $\to C\ 0\ \nil \to \Pi x: \vecc(U, n).(C\ n\ x)$

\noindent where $\mathsf{Ind}(U,n) := \lambda s. \lambda z. \lambda x. x\ s\ z$

\noindent $s :\Pi C: (\Pi p:\nat.\Pi q: \vecc(U, p). *).(\Pi m: \mathsf{Nat}.\Pi u:U.\forall y: \vecc(U,m).(  C \  m \ y \  \to C \ (\mathsf{S}m)\ (\mathsf{cons}\ m\ u\ y))), z: C\ 0\ \nil, x:  \vecc(U,n)$. 

\end{definition}

\begin{definition}[Append]
%%   \noindent $\app := \lambda n_1. \lambda n_2. \lambda l_1. \lambda l_2. l_1\ (\lambda n. \lambda x.\lambda v. \cons  (n+n_2)\ x\ v)\ l_2$.

%% \noindent  We can use induction to define append
%% as well.

\noindent $\tilde{\mu}_v \vdash \app : \Pi n_1:\mathsf{Nat}. \Pi n_2:\mathsf{Nat}. \vecc(U, n_1) \to \vecc(U, n_2) \to \vecc(U, n_1+n_2)$

\noindent where $\app := \lambda n_1. \lambda n_2.\lambda l_1.\lambda l_2. \mathsf{Ind}(U, n_1) (\lambda n. \lambda x.\lambda v. \cons  (n+n_2)\ x\ v)\ l_2 \ l_1$. 
%We can show that $\app : $
\end{definition}


\noindent \textbf{Typing}: We want to show $\app : \Pi n_1:\mathsf{Nat}. \Pi n_2:\mathsf{Nat}. \vecc(U, n_1) \to \vecc(U, n_2) \to \vecc(U, n_1+n_2)$. Observe that $\lambda n. \lambda x.\lambda v. \cons  (n+n_2)\ x\ v: \Pi n:\mathsf{Nat}. \Pi x:U. \vecc(U, n+n_2) \to \vecc(U, n+n_2+1) $. We instantiate $C :=  \lambda y.(\lambda x.\vecc(U, y + n_2))$ , where $x$ free over $\vecc(U, y + n_2)$, in $\mathsf{Ind}(U, n_1)$. By beta reductions, we get $\mathsf{Ind}(U, n_1) : (\Pi m: \mathsf{Nat}.\Pi u:U.\forall y: \vecc(U,m).(  \vecc(U, m + n_2)  \to \vecc(U, (\mathsf{S}m) + n_2)) \to \vecc(U, 0+n_2) \to \Pi x: \vecc(U, n_1). \vecc(U, n_1+n_2)$. 

\noindent So \small{$\mathsf{Ind}(U, n_1) \ (\lambda n. \lambda x.\lambda v. \cons  (n+n_2)\ x\ v) : \vecc(U, 0+n_2)  \to \Pi x: \vecc(U, n_1). \vecc(U, n_1+n_2) $}. We assume $l_1: \vecc(U, n_1), l_2:\vecc(U, n_2)$. Thus $\mathsf{ID}(U, n_1) \ (\lambda n. \lambda x.\lambda v. \cons  (n+n_2)\ x\ v) \ l_2 \ l_1: \vecc(U, n_1+n_2)$. 


\begin{theorem}[Associativity]
\

\noindent $\tilde{\mu}_v \vdash \Pi (n_1. n_2. n_3: \nat). \Pi(v_1: \vecc(U, n_1). v_2:\vecc(U, n_2).v_3:\vecc(U, n_3)).$

$ (\app \ n_1\ (n_2+n_3)\ v_1 \ (\app\ n_2\ n_3 \ v_2 \ v_3) = \app \ (n_1 + n_2) \ n_3\ (\app \ n_1 \ n_2 \ v_1 \ v_2) \ v_3$
\end{theorem}
\begin{proof}
  Use $\ind(U, n_1)$. We will not go through the proof here. 
\end{proof}


\section{Metatheory}
\label{s}
We will first outline the erasure from $\self$ to $\fomega$ with let-bindings, thus establishing
the strong normalization property for the terms. Note that we assume $\fomega$ with nonrecursive let-bindings is  consistent, since it can be easily reduced to $\fomega$ by substituting all the defined symbols with their defining terms. Since we are dealing with a Curry-style system, type preservation is a hard technical problem. We will then outline our method to prove type preservation for $\self$. The proofs in this section can be found in appendix \ref{es}, \ref{confana}, \ref{pres}.
\subsection{Erasure to $\fomega$}
\label{erasure}
The interesting cases in the following definition are highlighted in gray boxes. 
\begin{definition}[Erasure]
\

\footnotesize
\begin{tabular}{ll}
$F(*) \ := *$  

&

\gray{$F(\Pi x:T.\kappa) \ := F(\kappa)$}  

\\

$F(\Pi X:\kappa'.\kappa) \ := F(\kappa') \to F(\kappa)$  

&

\gray{$F(\mu \kappa)\ := F(\kappa)$}

\\

$F(X) \ := X$

&

\gray{$F(\iota x.T) \ := F(T)$}

\\

$F(\Pi X:\kappa.T) \ := \Pi X:F(\kappa). F(T)$

&

$F(\Pi x:T_1.T_2) \ :=  F(T_1) \to F(T_2)$

\\

\gray{$F(\forall x:T_1.T_2) \ := F(T_2)$}

&

$F(T_1 T_2) \ := F(T_1) F(T_2)$

\\

$F(\lambda X.T) \ := \lambda X. F(T)$

&

\gray{$F(T\ t) \ := F(T)$}

\\

\gray{$F(\lambda x.T) \ := F(T)$}

&

$F(\mu T) \ := F(\mu) F(T)$

\\

$F(x)\ := x$

&

$F(\lambda x.t)\ := \lambda x.F(t)$

\\

$F(t t') \ := F(t) F(t')$

&

$F(\mu t) \ := F(\mu) F(t)$

\\

$F(x_i \mapsto t_i, \mu) \ := x_i \mapsto F(t_i), F(\mu)$  

&

$F(X_i \mapsto T_i, \mu) \ := X_i \mapsto F(T_i), F(\mu)$  

\\
  $F((X:\kappa) \mapsto T, \Gamma) \ := X:F(\kappa) \mapsto F(T), F(\Gamma)$

&
  $F(X:\kappa, \Gamma)\ := X:F(\kappa), F(\Gamma)$
\\
  $F((x:T) \mapsto t, \Gamma) \ := x:F(T) \mapsto F(t), F(\Gamma)$
&
  $F(x:T, \Gamma) \ := x:F(T), F(\Gamma)$

\end{tabular}

\end{definition}
At term level, we have term $\mu t$, where $\mu$ may contain type definitions, thus we need to define erasure on terms as well. The erasure of $\iota x.T$ is $F(T)$: we simply erase all the terms at type level. With our restriction on closure, $F(\mu)$ will be an ordinary let-bindings.    

Let $\mathcal{M}_s, \mathcal{T}_s, \mathcal{K}_s, \Psi$ denote the set of terms, types, kinds and closures in $\mathbf{S}$, let $\mathcal{M}_{\omega},\mathcal{T}_{\omega}, \mathcal{K}_{\omega}, \Theta$ denote the set of terms, types, kinds and let-binding in $\fomega$. 


\begin{lemma}[Well-definedness of Erasure]
\

  \begin{enumerate}
  \item If $\kappa \in \mathcal{K}_s$, then $F(\kappa) \in \mathcal{K}_{\omega}$.
  \item If $t \in \mathcal{M}_s$, then $F(t) \in \mathcal{M}_{\omega}$.
  \item If $T \in \mathcal{T}_s$, then $F(T) \in \mathcal{T}_{\omega}$.
  \item If $\mu \in \Psi$, then $F(\mu) \in \Theta$.
  \end{enumerate}
\end{lemma}

\begin{lemma}
\label{subst3}
We have following equalities: $F(\kappa) \equiv F([t/x]\kappa)$, $F([T/X]\kappa) \equiv F(\kappa)$, $F([t/x]T) \equiv F(T)$, $F([T'/X]T) \equiv [F(T')/X]F(T)$ and $F([t'/x]t) \equiv [F(t')/x]F(t)$.
\end{lemma}
%% \begin{proof}
%% The first two equalities can be proved by induction on structure of $\kappa$(don't forget local property). For the third and fourth ones, by induction on structure of $T$. Of course, one would worry about cases like $\Pi X:\kappa. T$ and $\mu T$, it turns out that the local property of $\mu$ will help us through the second
%% case; for the first case, we rely on $F(\kappa)$ is a well-defined kind in \fomega.
%% \end{proof}

\begin{lemma}
\label{kind}
  If $\Gamma \vdash \kappa \cong \kappa'$, then $F(\kappa) \equiv F(\kappa')$.
\end{lemma}
%% \begin{proof}
%%   It suffices to show if $\Gamma \vdash \kappa \to_{o,\beta,\mu} \kappa'$, then $F(\kappa) \equiv F(\kappa')$.
%% So we proceed by induction on derivation of $\Gamma \vdash \kappa \to_{o,\beta,\mu} \kappa'$.
%% \end{proof}
Let $\hookrightarrow_{o,\beta,\mu}$ denote the reflexive closure of $\to_{o,\beta,\mu}$\footnote{$\to_{o,\beta,\mu}$ denotes $\to_{o} \cup \to_{\beta} \cup \to_{\mu}$. We will use this convention throughout the paper.}. 

\begin{lemma}
\label{inj}
  If $\Gamma \vdash T \to_{o,\beta,\mu} T'$, then $F(\Gamma) \vdash F(T) \hookrightarrow_{o,\beta,\mu} F(T')$.
\end{lemma}
\begin{proof}
  By induction on derivation of $\Gamma \vdash T \to_{o,\beta,\mu} T'$. We use lemma \ref{kind},
lemma \ref{subst3} above.
\end{proof}

\begin{lemma}
\label{Bij}
  If $\Gamma \vdash t \to_{\beta,\mu} t'$, then $F(\Gamma) \vdash F(t) \to_{\beta,\mu} F(t')$.
\end{lemma}
\begin{proof}
  By induction on derivation.
\end{proof}

Note that reductions inside the closure are not allowed. If one allows reduction inside closure, and then we would need to revise the lemma to: if $\Gamma \vdash t \to_{\beta,\mu} t'$, then $F(\Gamma) \vdash F(t) \hookrightarrow_{\beta,\mu} F(t')$. This means that the erasure erases some of the redex in the term, and then we would not be able to establish the strong normalization by the erasure theorem. 

\begin{theorem}[Erasure Theorem]
\label{erase}
\

  \begin{enumerate}
  \item   If $\Gamma \vdash T:\kappa$, then $F(\Gamma) \vdash F(T):F(\kappa)$.
  \item  If $\Gamma \vdash t:T$, then $F(\Gamma) \vdash F(t):F(T)$.
  \end{enumerate}
\end{theorem}

Lemma \ref{Bij} and Theorem \ref{erase} are essential to conclude strong normalization at term level, since all the reduction information at term level is preserved by the erasure function. However, at type level, we will not have strong normalization(observe the type of $\nat$ is diverging), yet $\self$ is still consistent in the sense that not every type is inhabited. %% \footnote{For readers who want to see the algorithmic typing, we provide an annotated version of the typing rules for $\self$ in appendix \ref{ann}.}
  


\subsection{About Type Preservation Proof}
In order to prove type preservation for $\self$, one needs to know how to combine pieces together. The complications are due to closure-related reductions together with several non-syntactic directed rules. We can prove preservation by adopting several techniques. Informally, one first needs to establish the confluence property for type level reductions, then we need a straightforward extension of Barendregt's method for proving Curry style \textbf{F} to handle the implicit product. Barendregt's method allows typing to \textit{quotient out} the \textit{transformations} of $\Pi X:\kappa.T$ and $\forall x:T.T'$. Then confluence for the type level reductions will ensure that if $\Pi x:T.T'$ can be transformed to $\Pi x:T_1.T_2$, then it must be that $T$ can be transformed to $T_1$ and $T'$ can be transformed to $T_2$. 
Thus, one establishes the so called \textit{compatibility} property for the explicit dependent types, which is the key to achieve type preservation. 

We will first prove several confluence results (this process is called \textit{confluence analysis}), then we develop a technique to quotient out the transformations of $\forall x:T.T'$ and $\Pi X:\kappa.T$ (called \textit{morph analysis}). Finally, we establish the compatibility theorem, which is enough for proving preservation.

We want to emphasize that we give the outline of the whole process because we want to convince readers that the method itself is worth noting and can be adapted to many other Curry-style systems with mutually recursive definitions.   
\subsection{Confluence Analysis}
\label{confanalysis}
First observe that the \textit{selfGen} rule and \textit{selfInst} rule are mutually inversed, so we can model the change of self type by the following rewriting point of view.

\begin{definition}
\

\noindent  $\Gamma \vdash T_1 \to_{\iota} T_2 $ if $T_1 \equiv \iota x.T' $ and $T_2 \equiv [t/x]T' $ for some fix $t \in \mathcal{M}_s$. 
\end{definition}

 Note that $\to_{\iota}$ models the \textit{selfInst} rule, $\to_{\iota}^{-1}$ models the \textit{selfGen} rule. Importantly, the notion of $\iota$-reduction does not build in structure congruent, namely, we do not allow reduction rules like: if $T \to_{\iota}T'$, then $\lambda x.T \to_{\iota} \lambda x.T'$. The purpose of $\iota$-reduction is to emulate the typing rule \textit{selfInst} and \textit{selfGen}. The goal of confluence analysis is to prove the following theorem.

\begin{theorem}[Fundamental Theorem]
\label{conf}
  $\to_{o,\iota,\beta,\mu}$ is confluent.
\end{theorem}

Of course, one can not prove this theorem by brute force. We will first show 
$\to_{\beta, \mu}$ is confluence by adopting Hardin's interpretation lemma, then we will make use of Hindley-Rossen's commutativity theorem to show $\to_o$ and $\to_{\iota}$ are by themself confluence and commute with $\to_{\beta, \mu}$. Thus we can conclude Theorem \ref{conf}. We use $\twoheadrightarrow$ to denote the reflexive symmetric transitive closure of $\to$.

\begin{lemma}[Interpretation lemma \cite{Hardin:1989}]
\label{interp}
Let $\to $ be $ \to_1 \cup \to_2$, 
$\to_1$ being confluent and strongly normalizing. We denote by $\nu(a)$ the $\to_1$-normal form of $a$. Suppose that there is some relation $\to_i$ on the $\to_1$-normal forms satisfying:

\

$\to_i \subseteq \twoheadrightarrow$, and $a \to_2 b $ implies $ \nu(a)   {\twoheadrightarrow_i}    \nu(b)$ $(\dagger)$

\

\noindent Then the confluence of $\to_i$ implies the confluence of $\to$.
\end{lemma}

\begin{proof}
 Suppose $\to_i$ is confluent. Assume $a  {\twoheadrightarrow}  a'$ and $a  {\twoheadrightarrow}  a''$. So by ($\dagger$), $\nu(a)  {\twoheadrightarrow_i}  \nu(a')$ and $\nu(a)  {\twoheadrightarrow_i}  \nu(a'')$. Note that $t  {\to_1^*}  t'$ implies $\nu(t) = \nu(t')$(By the confluence and strong normalization of $\to_1$). By the confluence of $\to_i$, there exists a $b$ such that $\nu(a')  {\twoheadrightarrow_i}  b$ and $\nu(a'')  {\twoheadrightarrow_i}  b$. Since $\to_i, \to_1 \subseteq \twoheadrightarrow$, we get $a' {\twoheadrightarrow}   \nu(a')  {\twoheadrightarrow}  b$ and $a'' {\twoheadrightarrow}   \nu(a'')  {\twoheadrightarrow}  b$. Hence $\to$ is confluent.

\begin{diagram}[size=2em,textflow]
& & & & a & & & &\\
& & &\ldLine &  & \rdLine & & &\\
& &\ldLine & &  & & \rdLine & &\\
&\ldOnto & & & \dDashtoo^1 &  &  & \rdOnto & \\
a'& &  & & \nu(a)  &  & & & a'' \\
&\rdDashtoo^1 &  &\ldDashtoo^i &   & \rdDashtoo^i  &  & \ldDashtoo^1 &\\
& & \nu(a')  &  &   &  & \nu(a'') & & \\
& &  & \rdDashtoo^i  &  & \ldDashtoo^i &   &  & \\
& &  &  & b  &   &  & & \\
\end{diagram}

\end{proof}

The reason that interpretation method works while the other direct methods fail is that it allows us to quotient out the $\to_1$-reduction, we only need to focus on proving the confluence of $\to_i$. This is 
essential because $\to_{\beta, \mu}$ can not be directly parallelized, namely, one can not use Tait-Martin L\"of's method (reported in \cite{Barendregt:1985}) directly to prove the confluence of $\to_{\beta, \mu}$, because the paralleled version does not enjoy diamond property. Interestingly, after modulo the $\to_{\mu}$-reduction, we introduce a new reduction $\to_{\beta\mu}$ (corresponds to $\to_i$), and we can then use the parallel reduction method to prove confluence of $\to_{\beta\mu}$.  


\begin{lemma}
\label{mu-sn}
  $\to_{\mu}$ is strongly normalizing and confluent.
\end{lemma}

So $\to_{\mu}$, $\to_{\beta}$ correspond to $\to_1$ and $\to_2$ in the interpretation lemma. Since $\to_{\mu}$ is strongly normalizing and confluent, we can define a normalization function which effectively computes the mu-normal form. 
 
\begin{definition}[Mu-normal Forms]
  \label{mu-normal}
\

\noindent Mu-normal Terms $n \ :: = \ x \ | \ \mu x_i \ | \ \lambda x.n \ | \ n n'$

\noindent Mu-normal Types $N  \:: = $

\noindent $ \ X \ | \ \mu X_i \ | \Pi x:N.N' \ | \ \iota x.N \ | \ \Pi X: K.N \ | \ \forall x:N.N' \ | \ N\ n \ | \ N N' \ | \ \lambda X.N \ | \ \lambda x.N$

\noindent Mu-normal Kinds $K \:: = \ * \ | \ \Pi x:N.K \ | \ \Pi X:K.K'$

\end{definition}

\noindent  \textbf{Note}: For the $\mu x_i$ and $\mu X_i$ in definition \ref{mu-normal}, we assume $x_i , X_i\in \mathrm{dom}(\mu)$. Let $\vec{\mu}t$ denote $\mu_1 ...\mu_n t$ with $n \geq 1$.

\begin{definition}[Normalization Function for Term]
  \

\small{
    \begin{tabular}{ll}

  $ \nu(x) \ : = \  x$

&

  $\nu(\lambda y.t)\ : = \ \lambda y.\nu(t)$

\\

  $\nu(t_1 t_2)\ : = \ \nu(t_1) \nu(t_2)$
&

 $ \nu(\vec{\mu}y) \ := y$ if $y \notin \mathrm{dom}(\vec{\mu})$

\\
  $ \nu(\vec{\mu}y) \ := \mu_i y$ if $y \in \mathrm{dom}(\mu_i)$

&
  $\nu(\vec{\mu}(t t')) \ :=  \nu(\vec{\mu} t) \nu( \vec{\mu}t')$

\\

  $\nu(\vec{\mu}( \lambda x.t)) \ := \lambda x.  \nu(\vec{\mu}t)$

\end{tabular}
}
\end{definition}

\begin{definition}[Normalization Function for Types]
\

\begin{tabular}{ll}
    $ \nu(X) \ : = \  X$
&
  $\nu(\lambda y.T)\ : = \ \lambda y.\nu(T)$
\\
  $\nu(T_1 T_2)\ : = \ \nu(T_1) \nu(T_2)$
&
$\nu(\lambda X.T)\ := \ \lambda X.\nu(T)$

\\

  $\nu(T t)\ : = \ \nu(T) \nu(t)$
&

  $\nu(\iota x.T)\ : = \ \iota x.\nu(T) $

\\

$\nu(\Pi X:\kappa.T)\ := \ \Pi X:\nu(\kappa). \nu(T)$

&

$\nu(\Pi x:T.T') \ := \ \Pi x:\nu(T). \nu(T')$
\\

$\nu(\forall x:T.T') \ := \ \forall x:\nu(T). \nu(T')$

&

 $ \nu(\vec{\mu}X) \ := X$ if $X \notin \mathrm{dom}(\vec{\mu})$

\\
  $ \nu(\vec{\mu}X) \ := \mu_i X$ if $X \in \mathrm{dom}(\mu_i)$
&
 
 $\nu(\vec{\mu}( \iota x.T)) \ := \iota x.  \nu(\vec{\mu}T)$

\\

  $\nu(\vec{\mu}( \Pi x:T.T')) \ := \Pi x:  \nu(\vec{\mu}T). \nu(\vec{\mu}T')$

&

  $\nu(\vec{\mu}( \forall x:T.T')) \ := \forall x:  \nu(\vec{\mu}T). \nu(\vec{\mu}T')$

\\

  $\nu(\vec{\mu}( \Pi X:\kappa.T')) \ := \Pi X:  \nu(\vec{\mu}\kappa). \nu(\vec{\mu}T')$
&

  $\nu(\vec{\mu}( T T')) \ :=  \nu(\vec{\mu}T) \nu(\vec{\mu}T')$

\\

  $\nu(\vec{\mu}( T t)) \ :=  \nu(\vec{\mu}T) \nu(\vec{\mu}t)$
&
  $\nu(\vec{\mu}( \lambda x.T)) \ :=  \lambda x. \nu(\vec{\mu}T)$

\\
$\nu(\vec{\mu}( \lambda X.T)) \ :=  \lambda X. \nu(\vec{\mu}T)$

\end{tabular}
\end{definition}

\begin{definition}[Normalization Function for Kinds]
  \

\small{
    \begin{tabular}{ll}

  $ \nu(*) \ : = \  *$

&

  $\nu(\Pi x:T.\kappa)\ : = \ \Pi x: \nu(T). \nu(\kappa)$
\\

  $\nu(\Pi X:\kappa'.\kappa)\ : = \ \Pi X: \nu(\kappa'). \nu(\kappa)$

&

  $\nu(\vec{\mu} *) \ :=  *$

\\

  $\nu(\vec{\mu}( \Pi x:T.\kappa)) \ := \Pi x:\nu(\vec{\mu}T). \nu(\vec{\mu}\kappa)$

&

  $\nu(\vec{\mu}( \Pi X:\kappa'.\kappa)) \ := \Pi X:\nu(\vec{\mu}\kappa'). \nu(\vec{\mu}\kappa)$

\end{tabular}
}
\end{definition}

%% \begin{proof}
%%   We will have to refer to the $\mathsf{Selfstar}$ paper for the proof of this theorem. Informally, the $\to_{\beta}, \to_{\mu}, \to_o, \to_{\iota}$ reductions in $\mathbf{S}$ are essentially same as the ones in $\mathsf{Selfstar}$, with only the differences that in $\mathsf{S}$, we distinguish
%% terms, types and kinds.  
%% \end{proof}

After the definitions of mu-normalization functions, we shall devise a new notion of reduction on mu-normal form, then show that this reduction is confluent (corresponds to $\to_i$ in the interpretation lemma and satisfying the $\dagger$ property), thus by the interpretation lemma, we can show $\to_{\beta, \mu}$ is confluent. A natural way to define reduction on mu-normal form is that right after a beta-reduction, one immediately mu-normalizes the contractum, which can form a notion of reduction on mu-normal form.  

\begin{definition}[$\beta$ Reduction on $\mu$-normal Forms]

\
\begin{tabular}{lll}
\infer{\Gamma \vdash n \to_{\beta \mu} \nu(t)}{\Gamma \vdash n \to_{\beta}t}

&

\infer{\Gamma \vdash N \to_{\beta \mu} \nu(T)}{\Gamma \vdash N \to_{\beta}T}

&

\infer{\Gamma \vdash K \to_{\beta \mu} \nu(\kappa')}{\Gamma \vdash K \to_{\beta}\kappa'}

\end{tabular}
\end{definition}

The following lemma shows that $\to_{\beta\mu}$ is indeed the reduction we want to fullfill the role of $\to_i$ in the interpretation lemma. 

\begin{lemma}
\label{fp}
\

\begin{itemize}
\item If $\Gamma \vdash t \to_{\beta} t'$, then $\Gamma \vdash \nu(t)\to_{\beta\mu} \nu(t')$.

\item If $\Gamma \vdash T \to_{\beta} T'$, then $\Gamma \vdash \nu(T)\to_{\beta\mu} \nu(T')$.

\item If $\Gamma \vdash \kappa \to_{\beta} \kappa'$, then $\Gamma \vdash \nu(\kappa)\to_{\beta\mu} \nu(\kappa')$.
\end{itemize}

\end{lemma}

\begin{lemma}
\label{mix}
$\to_{\beta\mu}$ is confluent.   
\end{lemma}

\begin{theorem}
  $\to_{\beta, \mu}$ is confluent.
\end{theorem}
\begin{proof}
  By lemma \ref{mu-sn}, lemma \ref{fp}, lemma \ref{mix} and the interpretation lemma.
\end{proof}

One can use the parallel reduction method to prove the confluence of $\to_{\beta\mu}$, while it is hard to directly prove the confluence of $\to_{\beta, \mu}$. Once we established the confluence of $\to_{\beta,\mu}$, it will be easier to analyze the interactions between $\to_{\beta,\mu}$ and
$\to_{\iota, o}$. We will make extensive use of the notion of \textit{commutativity}, which provides a simple way to analyze the confluence of a reduction system that has several confluent subreductons. 

\begin{theorem}
  $\to_{\iota}, \to_o$ both are confluent. 
\end{theorem}

\begin{definition}[Commutativity]
\noindent  Let $\to_1, \to_2$ be two notions of reduction. $\to_1$ (strong) commutes with $\to_2$ if the following diagram holds.

\

\begin{diagram}[size=1.5em,textflow]
 & & a & & \\
 & \ldTo_1 & & \rdTo_2 &  \\
 b & &  &  & c \\
 & \rdDashto_2 & & \ldDashto_1 &  \\
 & & d & & \\
\end{diagram}

\end{definition}

\begin{proposition}[Hindley-Rosen\footnote{ The proposition is taken from Barendregt's \cite{Barendregt:1985} Chapter 3.3, page 64.} ]
  Let $\to_1, \to_2$ be two notions of reduction. Suppose both $\to_1$ and $\to_2$ are
confluent, and $\to_1^*$ commutes with $\to_2^*$. Then $\to_1 \cup \to_2$ is confluent.
\end{proposition}


\begin{proposition}[Weak Commutativity\footnote{ The proposition is taken from Barendregt's \cite{Barendregt:1985} Chapter 3.3, page 65.}]
  Let $\hookrightarrow$ denote the reflexive closure of $\to$. Let $\to_1, \to_2$ be two notions of reduction. $\to_1$ weak commutes with $\to_2$ if the following diagram holds
\

\begin{diagram}[size=1.5em,textflow]
 & & a & & \\
 & \ldTo_1 & & \rdTo_2 &  \\
 b & &  &  & c \\
 & \rdDashInto_2 & & \ldDashtoo_1 &  \\
 & & d & & \\
\end{diagram}

\

If $\to_1$ weak commutes with $\to_2$, then $\to_1^*$ and $\to_2^*$ commute.
\end{proposition}

\begin{lemma}
  $\to_{\beta,\mu}$ commutes with $\to_{\iota}$. Thus $\to_{\beta, \mu, \iota}$ is confluent.
\end{lemma}

\begin{lemma}
  $\to_o$ commutes with $\to_{\iota}$, weak commutes with $\to_{\beta}$ and $\to_{\mu}$. 
\end{lemma}

\begin{theorem}[Fundamental Theorem]
  $\to_{o,\iota, \beta, \mu}$ is confluent.
\end{theorem}

The following theorem shows an application of fundamental theorem.

\begin{theorem}[$\iota$-elimination]
\label{invsc}
If $\Gamma \vdash \Pi x:T_1.T_2 =_{\beta,\mu,\iota,o} \Pi x:T_1'.T_2'$, then $\Gamma \vdash T_1 =_{\beta,\mu,o} T_1'$ and $\Gamma \vdash T_2 =_{\beta,\mu,o} T_2'$. 
\end{theorem}

\begin{proof}
  If $\Gamma \vdash \Pi x:T_1.T_2 =_{\beta,\mu,\iota,o} \Pi x:T_1'.T_2'$, then by the confluence of $\to_{\beta,\mu,\iota,o}$, there exists a $T$ such that $\Gamma \vdash \Pi x:T_1.T_2 (\to_{o, \iota,\beta,\mu})^* T$ and $\Gamma \vdash \Pi x:T_1'.T_2' (\to_{o, \iota,\beta,\mu})^* T$. Since all the reductions on $\Pi x:T_1.T_2$ preserve the structure of the dependent type, one will never have a chance to use $\to_{\iota}$-reduction, thus $\Gamma \vdash \Pi x:T_1.T_2 (\to_{o,\beta,\mu})^* T$ and $\Gamma \vdash \Pi x:T_1'.T_2' (\to_{o,\beta,\mu})^* T$. So $T$ must be of the form $\Pi x:T_3.T_4$. And $\Gamma \vdash T_1  (\to_{o,\beta,\mu})^* T_3$, $\Gamma \vdash T_1' (\to_{o,\beta,\mu})^* T_3$, $\Gamma \vdash T_2  (\to_{o,\beta,\mu})^* T_4$ and $\Gamma \vdash T_2' (\to_{o,\beta,\mu})^* T_4$. Finally, we have $\Gamma \vdash T_1 =_{\beta,\mu,o} T_1'$ and $\Gamma \vdash T_2 =_{\beta,\mu,o} T_2'$. 

\end{proof}

\subsection{Morph Analysis}
The confluence analysis and the rewriting point of view on the nonsyntactic directed rules can not be extended to deal with polymorphism. For example, $\Pi X:\kappa. X$ can be instantiated 
either to $T$ or to $T \to T$. So polymorphic instantiation as a rewrite relation is not confluent. The only known syntactic method\footnote{According to our knowlege.} to deal with preservation proof for Curry-style System \textbf{F} is Barendregt's method\cite{barendregt:1993}. We will extend his method to handle the instantiation of $\forall x:T.T'$. We call this style of analysis \textit{morph analysis}. 
 

\begin{definition}[Morphing Relations]
\

  \begin{itemize}
  \item $([\Gamma], T_1) \to_{i} ([\Gamma], T_2)$ if $T_1 \equiv \Pi X:\kappa.T' $ and $T_2 \equiv [T/X]T' $ for some $T$ such that $\Gamma \vdash T:\kappa$. 
  \item $([\Gamma,X:\kappa], T_1) \to_{g} ([\Gamma], T_2) $ if $T_2 \equiv \Pi X:\kappa.T_1$ and $\Gamma \vdash \kappa:\Box$.
  \item $([\Gamma], T_1) \to_{I} ([\Gamma], T_2) $ if $T_1 \equiv \forall x:T.T' $ and $T_2 \equiv [t/x]T' $ for some $t$ such that $\Gamma \vdash t:T$. 
  \item $([\Gamma, x:T], T_1) \to_{G} ([\Gamma], T_2) $ if $T_2 \equiv \forall x:T.T_1 $ and $\Gamma \vdash T:*$. 

  \end{itemize}
\end{definition}

One can view morphing relations as a way to model nonsyntactic directed typing rules. Note that morphing relations are not intended to be viewed as rewrite relation. Instead of proving confluence for these morphing relations, we try to use substitutions to \textit{summarize} the effects of a sequence of morphing relations. Before we do that, first we ``lift'' $=_{\mu,\beta,o,\iota}$ to 
a form of morphing relation.

\begin{definition}
  $([\Gamma], T) =_{\mu, \beta,o,\iota} ([\Gamma], T')$ if $\Gamma \vdash T =_{\mu, \beta,o,\iota} T'$ and $\Gamma \vdash T:*$ and $\Gamma \vdash T':*$.
\end{definition}

The best way to understand the following $E, G$ mapings is through understanding the lemma \ref{igelim} and the lemma \ref{IGelim}. They give concrete demonstrations of how to \textit{summarize} a sequence of morphing relations.

\begin{definition}
\

  \begin{tabular}{lll}
  $E(\Pi X:\kappa.T) := E(T)$
&
  $E(X) := X$

&

 $E(\Pi x:T_1. T_2) := \Pi x:T_1. T_2$

\\
$E(\lambda X.T) := \lambda X.T$

&

$E(T_1 T_2) := T_1 T_2$
&

$E(\forall x:T'.T) := \forall x:T'.T$

\\
$E(\iota x.T) := \iota x.T$

&
$E( T \ t) := T \ t$

&
$E(\lambda x.T) := \lambda x.T$

\\

$E(\mu T) := \mu T$

\end{tabular}
\end{definition}

\begin{definition}
\

  \begin{tabular}{lll}
  $G(\Pi X:\kappa.T) := \Pi X:\kappa.T$
&
  $G(X) := X$

&

 $G(\Pi x:T_1. T_2) := \Pi x:T_1. T_2$

\\
$G(\lambda X.T) := \lambda X.T$

&

$G(T_1 T_2) := T_1 T_2$
&

$G(\forall x:T'.T) := G(T)$

\\
$G(\iota x.T) := \iota x.T$

&
$G( T \ t) := T \ t$

&
$G(\lambda x.T) := \lambda x.T$

\\

$G(\mu T) := \mu T$
\end{tabular}
\end{definition}


\begin{lemma}
\label{subeg}
  $E([T'/X]T) \equiv [T''/X]E(T)$ for some $T''$; $G([t/x]T) \equiv [t/x]G(T)$ .
\end{lemma}
\begin{proof}
  By induction on the structure of $T$.
\end{proof}

\begin{lemma}
\label{igelim}
  If $([\Gamma], T) {\to_{i,g}^*} ([\Gamma'],T')$, then there exists a type substitution $\sigma$ such that $\sigma E(T) \equiv E(T')$. 
\end{lemma}
\begin{proof}
  It suffices to consider $([\Gamma],T) {\to_{i,g}} ([\Gamma'], T')$.
If $T' \equiv \Pi X:\kappa .T$ and $\Gamma = \Gamma',X:\kappa$, then $E(T') \equiv E(T)$.
If $T \equiv \Pi X:\kappa .T_1$ and $T' \equiv [T''/X]T_1$ and $\Gamma = \Gamma'$, then $E(T) \equiv E(T_1)$. By lemma \ref{subeg} above, we know $E(T') \equiv E([T''/X]T_1) \equiv [T_2/X]E(T_1)$ for some $T_2$. 
\end{proof}


\begin{lemma}
\label{IGelim}
  If $([\Gamma], T) {\to_{I,G}^*} ([\Gamma'], T')$, then there exists a term substitution $\delta$ such that $\delta G(T) \equiv G(T')$. 
\end{lemma}
\begin{proof}
  It suffices to consider $([\Gamma], T) {\to_{I,G}} ([\Gamma'], T')$.
If $T' \equiv \forall x:T_1 .T$ and $\Gamma = \Gamma',x:T_1$, then $G(T') \equiv G(T)$.
If $T \equiv \forall x:T_2 .T_1$ and $T' \equiv [t/x]T_1$ and $\Gamma = \Gamma'$, then $E(T) \equiv E(T_1)$. By lemma \ref{subeg} above, we know $E(T') \equiv E([t/x]T_1) \equiv [t/x]E(T_1)$. 
\end{proof}

\begin{lemma}
\label{typesub}
  If $([\Gamma],\Pi x:T_1. T_2) {\to_{i,g}^*} ([\Gamma'], \Pi x:T_1'.T_2')$, then there exists a type substitution $\sigma$ such that $\sigma(\Pi x:T_1.T_2) \equiv \Pi x:T_1'.T_2'$.
\end{lemma}

\begin{proof}
  By lemma \ref{igelim} above.
\end{proof}

\begin{lemma}
\label{termsub}
  If $([\Gamma], \Pi x:T_1. T_2) {\to_{I,G}^*} ([\Gamma'], \Pi x:T_1'.T_2')$, then there exists a term substitution $\delta$ such that $\delta(\Pi x:T_1.T_2) \equiv \Pi x:T_1'.T_2'$.
\end{lemma}

\begin{proof}
  By lemma \ref{IGelim} above.
\end{proof}

\noindent Let $\to_{o,\iota,\beta,\mu,i,g,I,G}^*$ denote $(\to_{i,g,I,G} \cup =_{o,\iota,\beta,\mu})^*$.
Let $\to_{o,\iota,\beta,\mu,i,g,I,G}$ denote $\to_{i,g,I,G} \cup =_{o,\iota,\beta,\mu}$. It is not exaggerated that the goal of confluence analysis and morph analysis is to establish the following \textit{compatibility} theorem. 

\begin{theorem}[Compatibility]
\label{comp}
  If $([\Gamma], \Pi x:T_1. T_2)  \to_{o,\iota,\beta,\mu,i,g,I,G}^* ([\Gamma'],\Pi x:T_1'. T_2')$, then there exists a mixed substitution\footnote{A substitution that contains both term substitution and type substitution.} $\phi$ such that $([\Gamma], \phi(\Pi x:T_1. T_2)) =_{o,\iota,\beta,\mu} ([\Gamma],\Pi x:T_1'.T_2')$. Thus $\Gamma \vdash \phi T_1 =_{o,\beta,\mu} T_1'$ and $\Gamma \vdash \phi T_2 =_{o,\beta,\mu} T_2'$(theorem \ref{invsc}).
\end{theorem}
\begin{proof}
By lemma \ref{termsub} and lemma \ref{typesub}. And we make use of the fact that if $\Gamma \vdash t =_{o,\iota,\beta,\mu} t'$, then for any mixed
substitution $\phi$, we have $\Gamma \vdash \phi t =_{o,\iota,\beta,\mu} \phi t'$.
\end{proof}

\subsection{Type Preservation Result}
\label{result}
%% \begin{lemma}
%% \label{type}
%%   Let $([\Gamma, \Delta], T_1) {\to_{o,\iota,\beta,\mu,i,g,I,G}}^* ([\Gamma], T_2)$. If $\Gamma, \Delta \vdash t:T_1$ with $\mathsf{dom}(\Delta) \# \mathsf{FV}(t)$, then $\Gamma \vdash t:T_2$. 
%% \end{lemma}

%% \noindent \textbf{Note}: We write $\stackrel{t}{\to}_{\beta,\mu,\iota,o, i, g, I, G}$ to means
%% the same thing as ${\to}_{\beta,\mu,\iota,o, i, g, I, G}^*$ with an emphasis on the subject $t$. 

%% \begin{lemma} 
%% \label{conv}
%%  If $([\Gamma], T_1) \stackrel{t}{\to}_{\beta,\mu,\iota,o, i, g, I, G} ([\Gamma'],T_2)$ and $\Gamma \vdash t =_{\beta,\mu} t'$, then $([\Gamma], T_1) \stackrel{t'}{\to}_{\beta,\mu,\iota,o, i, g, I, G} ([\Gamma'],T_2)$.  
%% \end{lemma} 
%% \begin{proof} By induction on length of $([\Gamma],T_1) \stackrel{t}{\to}_{\beta,\mu,\iota,o, i,g, I, G} ([\Gamma],T_2)$. Note that this lemma is \textbf{not} subject expansion, do not get confused.
%% \end{proof}


%% \begin{lemma} 
%%     \label{perm} If $\Gamma, \tilde{\mu}, y:T'
%% \vdash t:T$ , then $\Gamma, y: \mu  T',\tilde{\mu} 
%%  \vdash t :T$.  
%%  \end{lemma}
%% \begin{proof} By induction on the
%% derivation of $\Gamma, \tilde{\mu} , y:T' \vdash t:T$.
%% \end{proof}

%% \noindent \textbf{Note}: If $\Delta = x:T,..., X:\kappa$, then $\mu \Delta := x:\mu T,..., X:\mu \kappa$. 

%% \begin{lemma} 
%%     \label{metacong} 
%%     If $([\Gamma, \tilde{\mu}, \Delta], T) \stackrel{t}{\to}_{\beta,\mu,\iota,o, i, g, I, G} ([\Gamma, \tilde{\mu}, \Delta'], T')$ for some $\Delta, \Delta'$ and $\Gamma, \mu \Delta , \tilde{\mu}
%% \vdash \mathsf{ok}$, then 

%% \noindent $([\Gamma, \mu \Delta], \mu T) \stackrel{\mu t }{\to}_{\beta,\mu,\iota,o, i, g, I, G} ([\Gamma, \mu \Delta'], \mu T')$.
%%  \end{lemma} 

The proof of type preservation proceeds as usual. The inversion lemma and substitution lemma
are standard. Note that in the final preservation proof, we use the compatibility theorem.
 
\begin{lemma}[Inversion]

  \begin{itemize}
  \item If $\Gamma \vdash x:T$, then exist $\Delta, T_1$ such that $([\Gamma, \Delta], T_1) {\to_{o,\iota,\beta,\mu,i,g,I,G}^*} ([\Gamma], T)$ and $(x:T_1) \in \Gamma$.
 \item If $\Gamma \vdash t_1 t_2:T$, then exist $\Delta, T_1, T_2$ such that $\Gamma, \Delta \vdash t_1:\Pi x:T_1.T_2$ and $\Gamma, \Delta \vdash t_2:T_1$ and $([\Gamma, \Delta], [t_2/x]T_2) {\to_{o,\iota,\beta,\mu,i,g,I,G}^*} ([\Gamma],T)$. 

\item If $\Gamma \vdash \lambda x.t:T$, then exist $\Delta, T_1, T_2$ such that $\Gamma, \Delta , x:T_1 \vdash t:T_2$ and $([\Gamma, \Delta], \Pi x:T_1. T_2) {\to_{o,\iota,\beta,\mu,i,g,I,G}^*} ([\Gamma], T)$. 

\item If $\Gamma \vdash \mu t:T$, then exist $\Delta, T_1$ such that $\Gamma, \Delta, \tilde{\mu} \vdash t:T_1$ and $([\Gamma, \Delta], \mu T_1)$

$ {\to_{o,\iota,\beta,\mu,i,g,I,G}^*} ([\Gamma],T)$.
  \end{itemize}
\end{lemma}

\begin{lemma}[Substitution]
\label{subst1}
\

  \begin{enumerate}
  \item   If $\Gamma \vdash t:T$, then for any mixed substitution $\phi$ with $\mathrm{dom}(\phi) \# \mathrm{FV}(t) $, $\phi \Gamma \vdash t: \phi T$.
\item If $\Gamma, x:T \vdash t:T'$ and $\Gamma \vdash t':T$, then $\Gamma \vdash [t'/x]t:[t'/x]T'$.
  \end{enumerate}

\end{lemma}

\begin{proof}
  By induction on derivation.
\end{proof}

\begin{theorem}
  \label{presv}
  If $\Gamma \vdash t:T$ and $\Gamma \vdash t \to_{\beta, \mu} t'$ and $\Gamma \vdash \mathsf{wf}$, then $\Gamma \vdash t':T$.
\end{theorem}
\begin{proof}
  We list one interesting case:

\

\infer[\textit{App}]{\Gamma \vdash t t':[t'/x]T_2}{\Gamma
\vdash t:\Pi x:T_1.T_2 & \Gamma \vdash t': T_1}

\

\noindent Suppose $\Gamma \vdash (\lambda x.t_1) t_2 \to_{\beta} [t_2/x]t_1$. We know that
$\Gamma \vdash \lambda x.t_1 : \Pi x:T_1. T_2$ and $\Gamma \vdash t_2:T_1$. By
inversion on $\Gamma \vdash \lambda x.t_1 : \Pi x:T_1. T_2$, we know that 
there exist $\Delta, T_1', T_2'$ such that $\Gamma, \Delta, x:T_1' \vdash t_1:T_2'$
and $([\Gamma, \Delta], \Pi x:T_1'.T_2') {\to_{o,\iota,\beta,\mu,i,g,I,G}^*} ([\Gamma], \Pi x:T_1.T_2)$. 
By Theorem \ref{comp}, we have $([\Gamma, \Delta], \phi(\Pi x:T_1'.T_2')) =_{o,\iota,\beta,\mu} ([\Gamma, \Delta],\Pi x:T_1. T_2)$. By Church-Rosser
of $=_{o,\iota,\beta,\mu}$, we have $\Gamma, \Delta \vdash \phi T_1'=_{o,\beta,\mu}  T_1$ and $\Gamma, \Delta \vdash \phi T_2' =_{o,\beta,\mu} T_2$. 
So by (1) of lemma \ref{subst1}, we have $\Gamma,\phi(\Delta), x:\phi T_1' \vdash t_1: \phi T_2'$ with $\mathrm{dom}(\phi(\Delta)) \# (\mathrm{FV}(\phi T_1') \cup \mathrm{FV}(\phi T_2') \cup \mathrm{FV}(t_1)) $. So $\Gamma,\phi(\Delta), x: T_1 \vdash t_1: T_2$. Since $\Gamma \vdash t_2:T_1$, by (2) of lemma \ref{subst1}, $\Gamma, \phi(\Delta) \vdash [t_2/x]t_1: [t_2/x]T_2$. So we have $\Gamma\vdash [t_2/x]t_1: [t_2/x]T_2$ (by vacuously generalized and instantiated all the variables in $\mathrm{dom}(\phi(\Delta))$). 

\end{proof}

\section{$0 \not = 1$ in $\self$}
\label{zero}
The proof of $0 \not = 1$ follows the same method as in Theorem \ref{contract}, while the
argument for the uninhabitation of $\bot$ needs the erasure theorem and the preservation theorem. Notice that in this section, by $a = b$, we mean $\Pi C: (\Pi x:A.*). C\ a \to C\ b$ with $a, b :A$. 
\begin{definition}
  \
  
  $\bot := \Pi A:*.\forall x: A. \forall y:A. x = y$. 
\end{definition}

\begin{theorem}
 There is no term $t$ such that $ \tilde{\mu}_c \vdash t: \bot$
\end{theorem}
\begin{proof}
Suppose $\tilde{\mu}_c \vdash t: \bot$. By the erasure theorem (Theorem \ref{erase}) in section \ref{erasure}, then we have $ F(\tilde{\mu}_c)\vdash F(t) \equiv t:\Pi A:*. \Pi C:*. C \to C$ in $\fomega$ with let-bindings. $\Pi A:*.\Pi C:*. C \to C$ is the singleton type\footnote{Note that we are dealing with Curry-style $\fomega$.}, which is inhabited by $\lambda z.z$. This means $t \to_{\beta,\mu}^* \lambda z.z$ (the term reductions of $\fomega$ with let-bindings are the same as $\self$) and $\tilde{\mu}_c \vdash \lambda z.z: \bot$ in $\self$ (by type preservation, Theorem \ref{presv}). Then we would have $\tilde{\mu}_c, A:*, x:A,y:A,  C: (\Pi z:A. *), z: C\ x \vdash z :C\ y$. We know this derivation is impossible since $C\ x \not \cong C\ y$ by the confluence of $\cong$. 
  
\end{proof}
\begin{theorem}
$\tilde{\mu}_c \vdash 0 = 1 \to \bot$.
\end{theorem}
\begin{proof}
  This proof follows the method in Theorem \ref{contract}. Let $\Gamma = \tilde{\mu}_c, a : (\Pi B: (\Pi z:\nat. *). B 0 \to B 1), A:*, x:A, y:A, C:(\Pi z:A. *), c: C\ x$. We want to construct a term of type $C\ y$. Let $F := \lambda n[:\nat]. n\ [\lambda p:\nat. A]\ (\lambda q[:A].y) x$, note that 
  $F: \nat \to A$. We know that
 $F 0 =_{\beta} x$ and $F 1 =_{\beta} y$. So we can indeed convert the type of $c$ from $C x$ to $C\ (F 0)$. And then we instantiate the $B$ in $\Pi B:(\Pi z: \nat .*). B 0 \to B 1$ with $\lambda x[:\nat].C\ (F x)$. So we have $C\ (F 0) \to C\ (F 1)$ as the type of $a$. So $a c : C (F 1)$, which means $a c : C y$. So we just show how to inhabite $0 = 1 \to \bot$ in $\self$. 
\end{proof}

\section{Conclusion}
We propose System $\self$, which incorporates the self type construct together with implicit product and a restricted version of mutually recursion. Church-encoded datatypes and the corresponding induction principles are derivable within $\self$. With a change of notion of contradiction, we are able to show $0 \not = 1$ in both $\cc$ and $\self$. System $\self$ is consistent, since mutual recursiveness is only needed for the typing and the erasure of the recursive bindings becoming ordinary let-binding. We also demonstrate the process of proving the type preservation theorem, which is a hard problem for $\self$ due to the present of closures and the non-syntactic directed rules. 

%% \acks

%% Acknowledgments, if needed.

% We recommend abbrvnat bibliography style.

\bibliographystyle{plain}

% The bibliography should be embedded for final submission.
\bibliography{paper}
%% \begin{thebibliography}{}
%% \softraggedright

%% \bibitem[Smith et~al.(2009)Smith, Jones]{smith02}
%% P. Q. Smith, and X. Y. Jones. ...reference text...

%% \end{thebibliography}
\newpage
\appendix
\section{Coq Code}
\label{coq}
The following code formalizes the proof of theorem \ref{contract} in Coq.
\begin{verbatim}
Definition eq := 
  fun (A : Prop)(a b : A) => forall C : A -> Prop , C a -> C b.

Definition false := 
  forall A : Prop , forall a : A , forall b : A , eq A a b .

Definition Nat := forall A : Prop , (A -> A) -> A -> A.

Definition zero : Nat := fun (A : Prop)(s : A -> A)(z : A) => z.

Definition succ : Nat -> Nat := 
  fun (n:Nat)(A : Prop)(s : A -> A)(z : A) => s (n A s z).

Definition one : Nat := succ zero.

Theorem zeroNeqOne : eq Nat zero one -> false.
unfold false.
unfold eq.
intros u A a b C.
exact (u (fun (n:Nat) => C (n A (fun(q:A) => b) a))).
Qed.
\end{verbatim}

\section{Full Sepcifications of Reductions in $\self$}
\label{fullred}
\begin{definition}[Metalevel Abrieviation]
\

  \noindent \textit{Objects} $o \ ::= \ t \ | \ T \ | \ \kappa$

  \noindent \textit{Reduction Context} $\mathcal{C} \ ::=$

\noindent $ \bullet \ | \ \lambda x.\mathcal{C} \ | \ \mathcal{C} t'\ | \ t \mathcal{C}\ |\ \Pi X:\kappa.\mathcal{C} \ | \ \Pi x:T .\mathcal{C} \ |\ \Pi x:\mathcal{C}.T \ | \  \forall x:T .\mathcal{C} \ |\ \forall x:\mathcal{C}.T \ | \ \lambda X.\mathcal{C} \ | \ \iota x.\mathcal{C} \ | \ $

\noindent $T \mathcal{C} \ | \ \mathcal{C} T \ | \ \Pi x:\mathcal{C}.\kappa \ | \  \Pi X:\mathcal{C}. \kappa \ | \ \Pi x:\kappa.\mathcal{C} \ | \  \Pi X:\kappa. \mathcal{C}$

\end{definition}


\begin{definition}[Closure Reductions]
\

\footnotesize{
\begin{tabular}{lllll}


\infer{\Gamma \vdash \mu t \to_{o} t}{\mu \in \Gamma}

&

\infer{\Gamma \vdash \mu T \to_{o} T}{\mu \in \Gamma}

&

\infer{\Gamma \vdash \mu \kappa \to_{o} \kappa}{\mu \in \Gamma}

&

\infer{\Gamma \vdash \mu o \to_{o} \mu o'}{\Gamma, \tilde{\mu} \vdash o \to_{o} o'}

&
\infer{\Gamma \vdash \mathcal{C}[o] \to_{o} \mathcal{C}[o']}{\Gamma \vdash o \to_{o} o'}

\end{tabular}
}

\end{definition}

\noindent \textbf{Note}: Closure reducton is defined for type level only.
\begin{definition}[Beta Reductions]

\

\footnotesize{
\begin{tabular}{lll}


\infer{\Gamma \vdash x \to_{\beta} t}{(x\mapsto t) \in \Gamma}

&
\infer{\Gamma \vdash(\lambda x.t)t' \to_{\beta} [t'/x]t}{}

&

\infer{\Gamma \vdash\mu x_i \to_{\beta} \mu t_i}{(x_i \mapsto
t_i) \in \mu}
\\
\\

\infer{\Gamma \vdash(\lambda X.T)T' \to_{\beta} [T'/X]T}{}

&

\infer{\Gamma \vdash X \to_{\beta} T}{(X\mapsto T) \in \Gamma}

&
\infer{\Gamma \vdash(\lambda x.T)t \to_{\beta} [t/x]T}{}


\\
\\

\infer{\Gamma \vdash\mu X_i \to_{\beta} \mu T_i}{(X_i \mapsto
T_i) \in \mu}

&

\infer{\Gamma \vdash \mu o \to_{\beta} \mu o'}{\Gamma, \tilde{\mu} \vdash o \to_{\beta} o'  }

&

\infer{\Gamma \vdash \mathcal{C}[o] \to_{\beta} \mathcal{C}[o']}{\Gamma \vdash o \to_{\beta} o'}


%% \infer{\Gamma \vdash (\lambdabar x.t)\cdot t' \to_{\beta} [\underline{t}'/x]t}{}

\end{tabular}
}
  
\end{definition}

\begin{definition}[Mu Reductions]

\

\footnotesize{
\begin{tabular}{ll}


\infer{ \Gamma \vdash \mu t \to_{\mu} t}{\mathrm{dom}(\mu) \#
\mathrm{FV}(t)}

&
\infer{ \Gamma \vdash \mu(\lambda x.t) \to_{\mu} \lambda x.\mu
t}{}

\\
\\

\infer{ \Gamma \vdash \mu(t_1 t_2)  \to_{\mu} (\mu t_1 ) (\mu
t_2)}{}

&

\infer{ \Gamma \vdash \mu(T\ T') \to_{\mu} (\mu T)(\mu T')}{}
\\
\\

\infer{ \Gamma \vdash \mu T \to_{\mu} T}{\mathrm{dom}(\mu) \#
\mathrm{FV}(T)}

&

\infer{ \Gamma \vdash \mu(\iota x.T) \to_{\mu} \iota x.\mu T}{}

\\
\\

\infer{ \Gamma \vdash \mu(\forall x:T_1.T_2) \to_{\mu} \forall x:\mu T_1.\mu T_2}{}

&

\infer{ \Gamma \vdash \mu(\Pi X:\kappa.T) \to_{\mu} \Pi X:\mu \kappa.\mu T}{}

\\

\\

\infer{ \Gamma \vdash \mu(T\ t) \to_{\mu} (\mu T)(\mu t)}{}

&

\infer{ \Gamma \vdash \mu(\lambda X.T) \to_{\mu} \lambda X.\mu T}{}

\\
\\

\infer{ \Gamma \vdash \mu(\lambda x.T) \to_{\mu} \lambda x.\mu T}{}

&
\infer{ \Gamma \vdash \mu(\Pi x:T_1.T_2) \to_{\mu} \Pi x:\mu
T_1.\mu T_2}{}


\\
\\

\infer{ \Gamma \vdash \mu \kappa \to_{\mu} \kappa}{\mathrm{dom}(\mu) \#
\mathrm{FV}(\kappa)}

&

\infer{ \Gamma \vdash \mu(\Pi x:T.\kappa) \to_{\mu} \Pi x:\mu
T.\mu \kappa}{}

\\
\\

\infer{ \Gamma \vdash \mu(\Pi X:\kappa'.\kappa) \to_{\mu} \Pi X:\mu
\kappa'.\mu \kappa}{}

&

\infer{\Gamma \vdash \mu o \to_{\mu} \mu o'}{\Gamma, \tilde{\mu} \vdash o \to_{\mu} o'}

\\
\\

\infer{\Gamma \vdash \mathcal{C}[o] \to_{\mu} \mathcal{C}[o']}{\Gamma \vdash o \to_{\mu} o'}


\end{tabular}
}  
\end{definition}

\section{Full Specifications of $\fomega$ with Let-binding}
\label{fomega}

\begin{definition}[Syntax]

\

\noindent \textit{Terms} $t \ :: = \ x \ | \ \lambda x.t \ | \ t t'\ | \ {\rho} t$

\noindent \textit{Types} $T \ ::= \ X \ | \ \Pi X:\kappa.T \ | \ T_1 \to T_2 \ | \ \lambda X.T \ | \ T_1 T_2 \ | \ {\rho} T$

\noindent \textit{Kinds} $\kappa \ ::= \ * \ | \ \kappa' \to \kappa$ 

\noindent \textit{Context} $\Gamma \ :: = \ \cdot \ | \ \Gamma, x:T \ |  \ \Gamma, X:\kappa \ | \ \Gamma, \tilde{\rho}$ 

\noindent \textit{Let-binding} $\rho \ ::= \ \M{x}{t}{N}\cup \M{X}{T}{M}$

\end{definition} 

Note that for every $x \mapsto t, X \mapsto T \in \rho$, we require $\mathrm{FV}(t) = \emptyset$ and $\mathrm{FV}(T) = \emptyset$.

\begin{definition}[Metalevel Abrieviation]
\

\noindent \textit{Objects} $o \ ::= \ t \ | \ T$

  \noindent \textit{Reduction Context} $\mathcal{C} \ ::= \bullet \ | \ \lambda x.\mathcal{C} \ | \ \mathcal{C} t'\ | \ t \mathcal{C}\ | \ \Pi X:\kappa.\mathcal{C} \ | \ T \to \mathcal{C} \ |\ \mathcal{C} \to T \ | \ \lambda X.\mathcal{C} \ | \ T \mathcal{C} \ | \ \mathcal{C} T$

\end{definition}
\begin{definition}[Well-formed Context]
\

\footnotesize{
\begin{tabular}{lll}
\infer{ \cdot \vdash \mathsf{wf}}{}

&

\infer{ \Gamma, x:T \vdash \mathsf{wf}}{\Gamma \vdash \mathsf{wf} & \Gamma \vdash T:*}

&

\infer{\Gamma, \tilde{\rho} \vdash \mathsf{wf}}{\Gamma \vdash \mathsf{wf}
& \Gamma, \tilde{\rho} \vdash \mathsf{ok}}

\end{tabular}
}
\end{definition}


\begin{definition}[Kinding]
\

\footnotesize{
\begin{tabular}{lll}
\infer{\Gamma \vdash X:\kappa}{(X:\kappa) \in \Gamma}

&
%% \infer{\Gamma \vdash T : \kappa'}{\Gamma \vdash T:
%% \kappa & \Gamma \vdash \kappa \cong \kappa' & \Gamma \vdash \kappa': \Box}

%% &
\infer{\Gamma \vdash T_1 \to T_2 : *}{ \Gamma \vdash T_1 : * &
\Gamma \vdash T_2 : *}

&
\infer{\Gamma \vdash {\rho} T: \kappa}{\Gamma, \tilde{\rho}
\vdash T:\kappa & \Gamma, \tilde{\rho} \vdash \mathsf{ok}}

\\
\\
\infer{\Gamma \vdash \lambda X.T:\kappa\to \kappa'}{\Gamma, X:\kappa \vdash T : \kappa' }

&

\infer{\Gamma \vdash S T: \kappa}{\Gamma \vdash S: \kappa' \to \kappa & 
\Gamma \vdash T:\kappa'}

&

\infer{\Gamma \vdash \Pi X:\kappa. T : *}{ \Gamma, X:\kappa \vdash T : *}

\end{tabular}
}


\end{definition}

\begin{definition}[Typing Rules]
\

\footnotesize{
\begin{tabular}{ll}
    
\infer[\textit{Var}]{\Gamma \vdash x:T}{(x:T) \in \Gamma}

&
\infer[\textit{Conv}]{\Gamma \vdash t : T_2}{\Gamma \vdash t:
T_1 & \Gamma \vdash T_1 \cong T_2 & \Gamma \vdash T_2:*}

\\
\\

\infer[\textit{Func}]{\Gamma \vdash \lambda x.t : T_1 \to T_2}
{\Gamma, x:T_1 \vdash t: T_2 & \Gamma \vdash T_1:*}

&
\infer[\textit{App}]{\Gamma \vdash t t':T_2}{\Gamma
\vdash t: T_1 \to T_2 & \Gamma \vdash t': T_1}

\\
\\

\infer[\textit{Mu}]{\Gamma \vdash {\rho} t:\rho T} {\Gamma, \tilde{\rho}
\vdash t:T &  \Gamma, \tilde{\rho} \vdash \mathsf{ok}}
&

\infer[\textit{Poly}]{\Gamma \vdash  t :\Pi X:\kappa.T}
{\Gamma, X:\kappa \vdash t: T }

\\
\\

\infer[\textit{Inst}]{\Gamma \vdash t:[T'/X]T}{\Gamma \vdash t: \Pi X:\kappa.T 
& \Gamma \vdash T': \kappa}


\end{tabular}
}

\end{definition}

\noindent \textbf{Remarks} :

\begin{itemize}
  \item $\Gamma, \tilde{\rho} \vdash \mathsf{ok}$ stands for $\{\Gamma, \tilde{\rho} \vdash t_j: T_j\}_{(t_j:T_j) \in \tilde{\rho}}$ and $\{\Gamma, \tilde{\rho} \vdash T_j: \kappa_j\}_{(T_j:\kappa_j) \in \tilde{\rho}}$.
  \item $\cong $ is the reflexive transitive and symmetry closure of $\to_{\beta} \cup \to_o \cup \to_{\rho}$. 
  \item If $\rho$ is $\M{x}{t}{N}\cup \M{X}{T}{M}$, then $\tilde{\rho}$ is $\bm{x}{T}{t}{N} \cup \bm{X}{\kappa}{T}{M}$.

\end{itemize}

\begin{definition}[Closure Reductions]
\

\footnotesize{
\begin{tabular}{lll}


%% \infer{\Gamma \vdash \rho t \to_{o} t}{\rho \in \Gamma}

%% &

\infer{\Gamma \vdash \rho T \to_{o} T}{\rho \in \Gamma}


&

\infer{\Gamma \vdash \rho o \to_{o} \rho o'}{\Gamma, \tilde{\rho} \vdash o \to_{o} o'}

&

\infer{\Gamma \vdash \mathcal{C}[o] \to_{o} \mathcal{C}[o']}{\Gamma \vdash o \to_{o} o'}

\end{tabular}
}

\end{definition}

\noindent \textbf{Note}: Closure reduction is defined at type level and since terms will
not appear at type level in $\fomega$, we will not define $\to_o$ for term. 


\begin{definition}[Beta Reductions]

\

\footnotesize{
\begin{tabular}{llll}


\infer{\Gamma \vdash x \to_{\beta} t}{(x\mapsto t) \in \Gamma}

&
\infer{\Gamma \vdash(\lambda x.t)t' \to_{\beta} [t'/x]t}{}

&

\infer{\Gamma \vdash\rho x_i \to_{\beta} \rho t_i}{(x_i \mapsto
t_i) \in \rho}

&

\infer{\Gamma \vdash(\lambda X.T)T' \to_{\beta} [T'/X]T}{}

\\

\\


\infer{\Gamma \vdash X \to_{\beta} T}{(X\mapsto T) \in \Gamma}

&

\infer{\Gamma \vdash\rho X_i \to_{\beta} \rho T_i}{(X_i \mapsto
T_i) \in \rho}

&

\infer{\Gamma \vdash \rho o \to_{\beta} \rho o'}{\Gamma, \tilde{\rho} \vdash o \to_{\beta} o'}

&

\infer{\Gamma \vdash \mathcal{C}[o] \to_{\beta} \mathcal{C}[o']}{\Gamma \vdash o \to_{\beta} o'}

\end{tabular}
}
  
\end{definition}

\begin{definition}[Rho Reductions]

\

\footnotesize{
\begin{tabular}{lll}


\infer{ \Gamma \vdash \rho t \to_{\rho} t}{\mathrm{dom}(\rho) \#
\mathrm{FV}(t)}

&
\infer{ \Gamma \vdash \rho(\lambda x.t) \to_{\rho} \lambda x.\rho
t}{}

&

\infer{ \Gamma \vdash \rho(t_1 t_2)  \to_{\rho} (\rho t_1 ) (\rho
t_2)}{}

\\
\\

\infer{ \Gamma \vdash \rho(T\ T') \to_{\rho} (\rho T)(\rho T')}{}

&

\infer{ \Gamma \vdash \rho T \to_{\rho} T}{\mathrm{dom}(\rho) \#
\mathrm{FV}(T)}

&

\infer{ \Gamma \vdash \rho(\Pi X:\kappa.T) \to_{\rho} \Pi X:\rho \kappa.\rho T}{}

\\
\\

\infer{ \Gamma \vdash \rho(\lambda X.T) \to_{\rho} \lambda X.\rho T}{}

&


\infer{\Gamma \vdash \rho o \to_{\rho} \rho o'}{\Gamma, \tilde{\rho} \vdash o \to_{\rho} o'}
&

\infer{ \Gamma \vdash \rho(T_1 \to T_2) \to_{\rho} \rho T_1\to \rho T_2}{}

\\
\\

\infer{\Gamma \vdash \mathcal{C}[o] \to_{\rho} \mathcal{C}[o']}{\Gamma \vdash o \to_{\rho} o'}


\end{tabular}
}  
\end{definition}


\section{Proofs for Section \ref{erasure}}
\label{es}
\begin{lemma}
  If $\kappa \in \mathcal{K}_s$, then $F(\kappa) \in \mathcal{K}_{\omega}$.
\end{lemma}
\begin{proof}
  We prove this by induction on the structure of $\kappa$. 
\end{proof}


\begin{lemma}
\

  \begin{enumerate}
  \item If $t \in \mathcal{M}_s$, then $F(t) \in \mathcal{M}_{\omega}$.
  \item If $T \in \mathcal{T}_s$, then $F(T) \in \mathcal{T}_{\omega}$.
  \item If $\mu \in \Psi$, then $F(\mu) \in \Theta$.
  \end{enumerate}
\end{lemma}

\begin{proof}
We prove (1),(2) by induction on struture of $t,T$, we prove (3) by induction on the length
of $\mu$.

\
\begin{enumerate}
\item \noindent \textbf{Base Cases}: $t = x$. Obvious.
\item \noindent \textbf{Base Cases}: $T = X$. Obvious.
\item \noindent \textbf{Base Cases}: Suppose $\mu = x \mapsto t$, then by (1), we know $F(t) \in \mathcal{M}_{\omega}$. So $F(x \mapsto t) \in \Theta$. Suppose
$\mu = X \mapsto T$, then by (2), we know $F(T) \in \mathcal{T}_{\omega}$. So $F(X \mapsto T) \in \Theta$. 
\end{enumerate}

\begin{enumerate}

\item \noindent \textbf{Step Cases}: $t = \mu t'$. Then $F(t) = F(\mu)F(t')$. By (3), we know
that $F(\mu) \in \Theta$. By IH, we know $F(t') \in \mathcal{M}_{\omega}$. So $F(\mu)F(t') \in \mathcal{M}_{\omega}$.

\item \noindent \textbf{Step Cases}: $T = \mu T'$. Then $F(T) = F(\mu)F(T')$. By (3), we know
that $F(\mu) \in \Theta$. By IH, we know $F(T') \in \mathcal{T}_{\omega}$. So $F(\mu)F(T') \in \mathcal{T}_{\omega}$.

\item \noindent \textbf{Step Cases}: Suppose $\mu = x \mapsto t, \mu'$, then by IH, we know $F(\mu') \in \Theta$. By (1), we know that $F(t) \in \mathcal{M}_{\omega}$. So $F(x \mapsto t, \mu') \in \Theta$. Suppose $\mu = X \mapsto T, \mu'$, then by (2), we know $F(T) \in \mathcal{T}_{\omega}$. By IH, we know $F(\mu') \in \Theta$, So $F(X \mapsto T, \mu') \in \Theta$. 
\end{enumerate}
\end{proof}

%% \noindent \textbf{Remarks}: I believe above argument is valid, but I could not come up with a proper termination metric (to describe the bootstrap inducton on (1),(2)).


\begin{lemma}
\label{app:subst3}
$F(\kappa) \equiv F([t/x]\kappa)$, $F([T/X]\kappa) \equiv F(\kappa)$, $F([t/x]T) \equiv F(T)$ and $F([T'/X]T) \equiv [F(T')/X]F(T)$ and $F([t'/x]t) \equiv [F(t')/x]F(t)$.
\end{lemma}
\begin{proof}
The first two equalities can be proved by induction on structure of $\kappa$( we will use local property). For the third and fourth ones, by induction on structure of $T$. Of course, one would worry about cases like $\Pi X:\kappa. T$ and $\mu T$, it turns out that the local property of $\mu$ will help us through the second
case; for the first case, we rely on $F(\kappa)$ is a well-defined kind in $\fomega$.
\end{proof}

\begin{lemma}
\label{app:kind}
  If $\Gamma \vdash \kappa \cong \kappa'$, then $F(\kappa) \equiv F(\kappa')$.
\end{lemma}
\begin{proof}
  It suffices to show if $\Gamma \vdash \kappa \to_{o,\beta,\mu} \kappa'$, then $F(\kappa) \equiv F(\kappa')$.
So we proceed by induction on derivation of $\Gamma \vdash \kappa \to_{o,\beta,\mu} \kappa'$.
\end{proof}

\begin{lemma}
\label{app:inj}
  If $\Gamma \vdash T \to_{o,\beta,\mu} T'$, then $F(\Gamma) \vdash F(T) \hookrightarrow_{o,\beta,\mu} F(T')$.
\end{lemma}

\begin{proof}
  By induction on derivation of $\Gamma \vdash T \to_{o,\beta,\mu} T'$. We use lemma \ref{app:kind},
lemma \ref{app:subst3} above.
\end{proof}

\begin{theorem}
\

  \begin{enumerate}
  \item   If $\Gamma \vdash T:\kappa$, then $F(\Gamma) \vdash F(T):F(\kappa)$.
  \item  If $\Gamma \vdash t:T$, then $F(\Gamma) \vdash F(t):F(T)$.
  \end{enumerate}
\end{theorem}

\begin{proof}
  We prove the conjuction of (1) and (2). By induction on derivation. 

\

\noindent \textbf{Base Cases}: 

\

\begin{tabular}{ll}
\infer{\Gamma \vdash X:\kappa}{(X:\kappa) \in \Gamma}

&

\infer{\Gamma \vdash x:T}{(x:T) \in \Gamma}
  
\end{tabular}

\

\noindent Obvious.

\

\noindent \textbf{Step Case}: 

\

\infer{\Gamma \vdash \Pi X:\kappa. T : *}{ \Gamma, X:\kappa \vdash T : * & \Gamma \vdash \kappa:\Box}

\

\noindent By IH(1), we know $F(\Gamma), X:F(\kappa) \vdash F(T) : F(*)$. So $F(\Gamma) \vdash \Pi X:F(\kappa). F(T):*$.

\

\noindent \textbf{Step Case}: 

\

\infer{\Gamma \vdash \mu T: \mu \kappa}{\Gamma, \tilde{\mu}
\vdash T:\kappa & \Gamma, \tilde{\mu} \vdash \mathsf{ok}}

\

\noindent Recall that $\Gamma, \tilde{\mu} \vdash \mathsf{ok}$ stands for $\{\Gamma, \tilde{\mu} \vdash t_j: T_j\}_{(t_j:T_j) \in \tilde{\mu}}$ and $\{\Gamma, \tilde{\mu} \vdash T_j: \kappa_j\}_{(T_j:\kappa_j) \in \tilde{\mu}}$. By IH(1) and (2), we know $F(\Gamma), F(\tilde{\mu}) \vdash F(T):F(\kappa)$ 
and $\{F(\Gamma), F(\tilde{\mu}) \vdash F(t_j): F(T_j)\}_{(F(t_j):F(T_j)) \in F(\tilde{\mu})}$ and $\{F(\Gamma), F(\tilde{\mu}) \vdash F(T_j): F(\kappa_j)\}_{(F(T_j):F(\kappa_j)) \in F(\tilde{\mu})}$. So we have $F(\Gamma) \vdash F(\mu T) \equiv F(\mu)F(T): F(\kappa)$ by the kinding rule in $\fomega$. Note that $F(\mu) \equiv |F(\tilde{\mu})|$, where $|\cdot|$ deletes all the type annotations.

\

\noindent \textbf{Step Case}: 

\

\infer{\Gamma \vdash \iota x.T : *}{\Gamma,
x:\iota x.T \vdash T : * }

\

\noindent By IH(1), we know $F(\Gamma), x:F(T) \vdash F(T) : *$. Since $x \notin \mathrm{FV}(F(T))$, we have $F(\Gamma) \vdash F(T):*$. 

\

\noindent \textbf{Step Case}: 

\

\infer{\Gamma \vdash \lambda X.T: \Pi X:\kappa. \kappa'}{\Gamma, X:\kappa \vdash T : \kappa' & \Gamma \vdash \kappa : \Box }

\

\noindent By IH(1), we know $F(\Gamma), X:F(\kappa) \vdash F(T) : F(\kappa')$. So $F(\Gamma) \vdash \lambda X.F(T): F(\kappa) \to F(\kappa')$. 

\

\noindent \textbf{Step Case}: 

\

\infer{\Gamma \vdash \lambda x.T: \Pi x:T'.\kappa}{\Gamma, x:T' \vdash T : \kappa & \Gamma \vdash T':*}

\

\noindent By IH(1), we have $F(\Gamma), x:F(T') \vdash F(T ): F(\kappa)$. Since $x \notin \mathrm{FV}(F(T))$, we know $F(\Gamma) \vdash F(T ): F(\kappa)$. 

\

\noindent \textbf{Step Case}: 

\

\infer{\Gamma \vdash S t: [t/x]\kappa}{\Gamma \vdash S: \Pi x:T.\kappa & 
\Gamma \vdash t:T}

\

\noindent By IH(1), we have $F(\Gamma) \vdash F(S): F(\kappa)$. Then we use the fact that $F(\kappa) \equiv F([t/x]\kappa)$. 

\

\noindent \textbf{Step Case}: 

\

\infer{\Gamma \vdash S T: [T/X]\kappa}{\Gamma \vdash S: \Pi X:\kappa'.\kappa & 
\Gamma \vdash T:\kappa'}

\

\noindent By IH(1), we have $F(\Gamma) \vdash F(S):F(\kappa')\to F(\kappa)$ and $F(\Gamma) \vdash F(T):F(\kappa')$. So $F(\Gamma) \vdash F(S) F(T) : F(\kappa)$. Then we use the fact that
$F([T/X]\kappa) \equiv F(\kappa)$.

\

\noindent \textbf{Step Case}: 

\

\infer{\Gamma \vdash \forall x:T_1.T_2 : *}{ \Gamma, x:T_1 \vdash T_2 : * &
\Gamma \vdash T_1 : *}

\

\noindent By IH(1), we know $F(\Gamma), x:F(T_1) \vdash F(T_2) : *$. Since $x \notin \mathrm{FV}(F(T_2))$, we have $F(\Gamma) \vdash F(T_2) : *$.

\

\noindent \textbf{Step Case}: 

\

\infer[\textit{Conv}]{\Gamma \vdash t : T_2}{\Gamma \vdash t:
T_1 & \Gamma \vdash T_1 \cong T_2 & \Gamma \vdash T_2:*}

\

\noindent By lemma \ref{app:inj} and IH(2).

\

\noindent \textbf{Step Case}: 

\

\infer[\textit{SelfGen}]{\Gamma \vdash t : \iota x.T}{\Gamma
\vdash t: [t/x]T & \Gamma \vdash \iota x.T: *}

\

\noindent By IH(2) and lemma \ref{app:subst3}, we know $F(\Gamma) \vdash F(t): F(T)$.

\

\noindent \textbf{Step Case}: 

\

\infer[\textit{SelfInst}]{\Gamma \vdash t: [t/x]T}{\Gamma
\vdash t : \iota x.T}

\

\noindent By IH(2) and lemma \ref{app:subst3}, we know $F(\Gamma) \vdash F(t): F(T)$.

\

\noindent \textbf{Step Case}: 

\

\infer[\textit{Indx}]{\Gamma \vdash t : \forall x:T_1.T_2}
{\Gamma, x:T_1 \vdash t: T_2 & \Gamma \vdash T_1:* & x \notin \mathrm{FV}(t)}

\

\noindent By IH(2), we know $F(\Gamma), x:F(T_1) \vdash F(t): F(T_2)$. Since $x \notin \mathrm{FV}(t)$, thus $x \notin \mathrm{FV}(F(t))$, so we get $F(\Gamma) \vdash F(t): F(T_2)$.

\

\noindent \textbf{Step Case}: 

\

\infer[\textit{Dex}]{\Gamma \vdash t :[t'/x]T_2}{\Gamma
\vdash t: \forall x:T_1.T_2 & \Gamma \vdash t': T_1}

\

\noindent By IH(2) and lemma \ref{app:subst3}, we know $F(\Gamma) \vdash F(t): F(T_2)$. 

\

\noindent \textbf{Step Case}: 

\

\infer[\textit{Mu}]{\Gamma \vdash \mu t: \mu T}{\Gamma, \tilde{\mu}
\vdash t:T &  \Gamma, \tilde{\mu} \vdash \mathsf{ok}}

\

\noindent Recall that $\Gamma, \tilde{\mu} \vdash \mathsf{ok}$ stands for $\{\Gamma, \tilde{\mu} \vdash t_j: T_j\}_{(t_j:T_j) \in \tilde{\mu}}$ and $\{\Gamma, \tilde{\mu} \vdash T_j: \kappa_j\}_{(T_j:\kappa_j) \in \tilde{\mu}}$. By (1), IH(2), we know $F(\Gamma), F(\tilde{\mu}) \vdash F(t):F(T)$ 
, $\{F(\Gamma), F(\tilde{\mu}) \vdash F(t_j): F(T_j)\}_{(F(t_j):F(T_j)) \in F(\tilde{\mu})}$ and $\{F(\Gamma), F(\tilde{\mu}) \vdash F(T_j): F(\kappa_j)\}_{(F(T_j):F(\kappa_j)) \in F(\tilde{\mu})}$. So we have $F(\Gamma) \vdash F(\mu)F(t) \equiv F(\mu t): F(\mu T) \equiv F(\mu)F(T)$ by the rule in $\fomega$. Note that $F(\mu) \equiv |F(\tilde{\mu})|$, where $|\cdot|$ deletes all the type annotations.

\

\noindent \textbf{Step Case}: 

\

\infer[\textit{Poly}]{\Gamma \vdash  t :\Pi X:\kappa.T}
{\Gamma, X:\kappa \vdash t: T & \Gamma \vdash \kappa:\Box}

\

\noindent By IH(2), we know $F(\Gamma), X:F(\kappa) \vdash F(t):F(T)$, so $F(\Gamma) \vdash  F(t) :\Pi X:F(\kappa).F(T)$.

\

\noindent \textbf{Step Case}: 

\


\infer[\textit{Inst}]{\Gamma \vdash t:[T'/X]T}{\Gamma \vdash t: \Pi X:\kappa.T 
& \Gamma \vdash T': \kappa}

\

\noindent By IH(2) and (1), we know $F(\Gamma) \vdash  F(t) :\Pi X:F(\kappa).F(T)$ and $F(\Gamma) \vdash F(T'):F(\kappa)$. So $F(\Gamma) \vdash  F(t) : [F(T')/X]F(T) \equiv F([T'/X]T)$(lemma \ref{app:subst3}).

\

\noindent \textbf{Step Case}: 

\

\infer[\textit{Func}]{\Gamma \vdash \lambda x.t : \Pi x:T_1. T_2}
{\Gamma, x:T_1 \vdash t: T_2 & \Gamma \vdash T_1:*}

\

\noindent By IH(2) and (1), we know $F(\Gamma), x:F(T_1) \vdash F(t): F(T_2)$ and $F(\Gamma) \vdash F(T_1):*$. So $F(\Gamma) \vdash \lambda x.F(t) \equiv F(\lambda x.t): F(T_1) \to F(T_2) \equiv F(\Pi x:T_1. T_2)$.

\

\noindent \textbf{Step Case}: 

\

\infer[\textit{App}]{\Gamma \vdash t t':[t'/x]T_2}{\Gamma
\vdash t: \Pi x:T_1. T_2 & \Gamma \vdash t': T_1}

\

\noindent By IH(2), we have $F(\Gamma) \vdash F(t):F(T_1)\to F(T_2) $ and $ F(\Gamma) \vdash F(t'): F(T_1)$. So $F(\Gamma) \vdash F(t t') \equiv F(t)F(t'): F(T_2) \equiv F([t'/x]T_2)$(lemma \ref{app:subst3}).

\end{proof}

\section{Proofs for Section \ref{confanalysis}}
\label{confana}
Let $\vec{\mu}t$ denote $\mu_1 ...\mu_n t$ where $n \geq 1$, we write $\dot{\vec{\mu}}t$ for 
$n \geq 0$. 

\begin{lemma}
    \label{norm:sub}
$\nu(\vec{\mu}\vec{\mu}o) \equiv \nu(\vec{\mu}o)$, $\nu(\vec{\mu} ([o_2/x]o_1)) \equiv \nu( [\vec{\mu} o_2/x]\vec{\mu} o_1)$ and  $\nu(\vec{\mu} ([o_2/X]o_1)) \equiv \nu( [\vec{\mu} o_2/X]\vec{\mu} o_1)$
\end{lemma}

\begin{lemma}
\label{norm:iden}
 $\nu(\nu(o)) \equiv \nu(o)$, $\nu([\nu(o_1)/y] \nu(o_2)) \equiv \nu([o_1/y]o_2)$ and $\nu([\nu(o_1)/X] \nu(o_2)) \equiv \nu([o_1/X]o_2)$. 
\end{lemma}

In order to prove lemma \ref{fp}, we prove a generalized version.

\begin{lemma}
\label{app:fp}
\

\begin{itemize}
\item If $\Gamma, \dot{\vec{\mu}} \vdash t \to_{\beta} t'$, then $\Gamma \vdash \nu(\dot{\vec{\mu}} t)\to_{\beta\mu} \nu( \dot{\vec{\mu}} t')$.

\item If $\Gamma, \dot{\vec{\mu}} \vdash T \to_{\beta} T'$, then $\Gamma \vdash \nu(\dot{\vec{\mu}}T)\to_{\beta\mu} \nu(\dot{\vec{\mu}}T')$.

\item If $\Gamma, \dot{\vec{\mu}} \vdash \kappa \to_{\beta} \kappa'$, then $\Gamma \vdash \nu(\dot{\vec{\mu}}\kappa)\to_{\beta\mu} \nu(\dot{\vec{\mu}} \kappa')$.
\end{itemize}

\end{lemma}

\begin{proof}
  By induction on derivation of $\Gamma, \dot{\vec{\mu}} \vdash o \to_{\beta}o'$. 

\noindent \textbf{Base Case:}

\

\noindent \infer{\Gamma, \dot{\vec{\mu}} \vdash x \rightarrow_{\beta}  t}{(x \mapsto t) \in \Gamma, \dot{\vec{\mu}}}

\

\noindent If $x \mapsto t \in \dot{\vec{\mu}}$, then $\Gamma \vdash \nu(\dot{\vec{\mu}}x) \equiv  \mu x \to_{\beta\mu} \nu(\mu t) \equiv \nu(\dot{\vec{\mu}} t)$. Techincally, the last equality need to be justified, we can justify that by locality of $\mu$.  If $x \mapsto t \in \Gamma$, then $\Gamma \vdash \nu(\dot{\vec{\mu}}x) \equiv x \to_{\beta\mu} \nu(t) \equiv \nu(\dot{\vec{\mu}} t)$. 

\

\noindent \textbf{Base Case:}

\

\noindent \infer{\Gamma,\dot{\vec{\mu}} \vdash \mu x_i \to_{\beta} \mu t_i}{(x_i \mapsto t_i) \in \mu}

\

\noindent We have $\Gamma \vdash \nu(\dot{\vec{\mu}}\mu x_i) \equiv \mu x_i \to_{\beta\mu} \nu(\mu  t_i) \equiv \nu(\dot{\vec{\mu}} \mu t_i)$.

\

\noindent \textbf{Base Case:}

\

\noindent \infer{\Gamma, \dot{\vec{\mu}} \vdash (\lambda x.t)t' \to_{\beta} [t'/x]t}{}

\

\noindent We have $\Gamma \vdash \nu(\dot{\vec{\mu}}((\lambda x.t)t')) \equiv (\lambda x.\nu(\dot{\vec{\mu}}t))\nu(\dot{\vec{\mu}}t') \to_{\beta\mu} \nu([\nu(\dot{\vec{\mu}}t)/x]\nu(\dot{\vec{\mu}}t')) \equiv \nu([\dot{\vec{\mu}}t/x]\dot{\vec{\mu}}t') \equiv \nu(\dot{\vec{\mu}}([t'/x]t))$. The last two equalities are by lemma \ref{norm:iden}, lemma \ref{norm:sub}. 

\

\noindent \textbf{Step Case:}

\

\noindent \infer{\Gamma, \dot{\vec{\mu}} \vdash \mathcal{C}[o] \to_{\beta} \mathcal{C}[o']}{\Gamma, \dot{\vec{\mu}} \vdash o \to_{\beta}o' }

\

\noindent $\Gamma \vdash \nu(\dot{\vec{\mu}}(\mathcal{C}[o]))  \equiv  \mathcal{C}[\nu(\dot{\vec{\mu}}o)]  \stackrel{IH}{\to_{\beta\mu}} \mathcal{C}[\nu(\dot{\vec{\mu}} o')] \equiv \nu(\dot{\vec{\mu}}(\mathcal{C}[o'])) $. 

\

\noindent \textbf{Step Case:}

\

\noindent \infer{\Gamma, \dot{\vec{\mu}} \vdash \mu o \to_{\beta} \mu o'}{\Gamma,\dot{\vec{\mu}} ,\tilde{\mu} \vdash o \to_{\beta}o' }

\

\noindent We want to show $\Gamma \vdash  \nu(\dot{\vec{\mu}} \mu o) \to_{\beta\mu} \nu(\dot{\vec{\mu}} \mu o')$. This is directly by IH. 

\

\noindent All the other cases are similar.
\end{proof}

We will use Tait-Martin L\"of's parallel reduction method to prove lemma \ref{mix}. Recall the definition of the $\to_{\beta\mu}$:

\begin{definition}[$\beta$ Reduction on $\mu$-normal Forms]

\
\begin{tabular}{lll}
\infer{\Gamma \vdash n \to_{\beta \mu} \nu(t)}{\Gamma \vdash n \to_{\beta}t}

&

\infer{\Gamma \vdash N \to_{\beta \mu} \nu(T)}{\Gamma \vdash N \to_{\beta}T}

&

\infer{\Gamma \vdash K \to_{\beta \mu} \nu(\kappa')}{\Gamma \vdash K \to_{\beta}\kappa'}

\end{tabular}
\end{definition}

Now let us define the notion of parallel reduction w.r.t. $\to_{\beta\mu}$.

\begin{definition}[Parallel Reductions]

\

\centering
\footnotesize
  \begin{tabular}{ll}


\infer{\Gamma \vdash  n \Rightarrow_{\beta \mu} n}{}

&
\infer{\Gamma \vdash  x \Rightarrow_{\beta\mu} \nu( t)}{(x \mapsto t) \in \Gamma}

\\
\\

\infer{\Gamma \vdash (\lambda x.n_1) n_2 \Rightarrow_{\beta\mu} \nu([n_2'/x]n_1')}{\Gamma \vdash   n_1\Rightarrow_{\beta\mu} n_1' &\Gamma \vdash  n_2\Rightarrow_{\beta\mu} n_2'}

&

\infer{\Gamma \vdash \mu x_i \Rightarrow_{\beta\mu} \nu(\mu t_i)}{(x_i \mapsto t_i) \in \mu}

\\
\\

\infer{\Gamma \vdash \lambda x.n \Rightarrow_{\beta\mu} \lambda x.n'}{\Gamma \vdash n \Rightarrow_{\beta\mu}n' }

&

\infer{\Gamma \vdash n n' \Rightarrow_{\beta\mu} n'' n'''}{ \Gamma \vdash  n \Rightarrow_{\beta\mu}n''& \Gamma \vdash n' \Rightarrow_{\beta\mu} n'''}

\\
\\

\infer{\Gamma \vdash \iota x.N \Rightarrow_{\beta\mu} \iota x.N'}{\Gamma \vdash N \Rightarrow_{\beta\mu}N' }

&
\infer{\Gamma \vdash \Pi x:N.N' \Rightarrow_{\beta\mu} \Pi x:N''.N'''}
{\Gamma \vdash N' \Rightarrow_{\beta\mu} N''' &\Gamma \vdash  N \Rightarrow_{\beta\mu}N'' }

\\
\\

\infer{\Gamma \vdash \lambda x.N \Rightarrow_{\beta\mu} \lambda x.N'}{\Gamma \vdash N \Rightarrow_{\beta\mu}N' }

&

\infer{\Gamma \vdash \lambda X.N \Rightarrow_{\beta\mu} \lambda X.N'}{\Gamma \vdash N \Rightarrow_{\beta\mu}N' }

\\
\\

\infer{\Gamma \vdash  N \Rightarrow_{\beta \mu} N}{}

&
\infer{\Gamma \vdash  X \Rightarrow_{\beta\mu} \nu(T)}{(X \mapsto T) \in \Gamma}

\\
\\

\infer{\Gamma \vdash (\lambda X.N_1) N_2 \Rightarrow_{\beta\mu} \nu([N_2'/X]N_1')}{\Gamma \vdash   N_1\Rightarrow_{\beta\mu} N_1' &\Gamma \vdash  N_2\Rightarrow_{\beta\mu} N_2'}

&

\infer{\Gamma \vdash \mu X_i \Rightarrow_{\beta\mu} \nu(\mu T_i)}{(X_i \mapsto T_i) \in \mu}

\\
\\
\infer{\Gamma \vdash (\lambda x.N_1) n_2 \Rightarrow_{\beta\mu} \nu([n_2'/x]N_1')}{\Gamma \vdash   N_1\Rightarrow_{\beta\mu} N_1' &\Gamma \vdash  n_2\Rightarrow_{\beta\mu} n_2'}

&
\infer{\Gamma \vdash \forall x:N.N' \Rightarrow_{\beta\mu} \forall x:N''.N'''}
{\Gamma \vdash N' \Rightarrow_{\beta\mu} N''' &\Gamma \vdash  N \Rightarrow_{\beta\mu}N'' }

\\
\\

\infer{\Gamma \vdash N n \Rightarrow_{\beta\mu} N' n'}{ \Gamma \vdash  N \Rightarrow_{\beta\mu}N'& \Gamma \vdash n \Rightarrow_{\beta\mu} n'}


&

\infer{\Gamma \vdash N N' \Rightarrow_{\beta\mu} N'' N'''}{ \Gamma \vdash  N \Rightarrow_{\beta\mu}N''& \Gamma \vdash N' \Rightarrow_{\beta\mu} N'''}

\\

\\


\infer{\Gamma \vdash \Pi x:K.N' \Rightarrow_{\beta\mu} \Pi x:K'.N'''}
{\Gamma \vdash N' \Rightarrow_{\beta\mu} N''' &\Gamma \vdash  K \Rightarrow_{\beta\mu}K' }

&


\infer{\Gamma \vdash  K \Rightarrow_{\beta \mu} K}{}

\\
\\
\infer{\Gamma \vdash \Pi x:N.K \Rightarrow_{\beta\mu} \Pi x:N'.K'}
{\Gamma \vdash N \Rightarrow_{\beta\mu} N' &\Gamma \vdash  K \Rightarrow_{\beta\mu}K' }

&

\infer{\Gamma \vdash \Pi X:K.K' \Rightarrow_{\beta\mu} \Pi X:K''.K'''}
{\Gamma \vdash K \Rightarrow_{\beta\mu} K'' &\Gamma \vdash  K' \Rightarrow_{\beta\mu}K''' }

\end{tabular}

\end{definition}


\begin{lemma}
  \label{sub}
  $\to_{\beta\mu} \subseteq \Rightarrow_{\beta\mu} \subseteq \to_{\beta\mu}^*$.
\end{lemma}

\begin{lemma}
\label{lemma7}
If $\Gamma \vdash o_2 \Rightarrow_{\beta\mu} o_2'$, then $\Gamma \vdash \nu([o_2/x]o_1) \Rightarrow_{\beta\mu} \nu([o_2'/x]o_1)$ and $\Gamma \vdash \nu([o_2/X]o_1) \Rightarrow_{\beta\mu} \nu([o_2'/X]o_1)$.
\end{lemma}

\begin{proof}
\noindent  By induction on the structure of $o_1$. 

\

\noindent \textbf{Base Cases}: $o_1= x, \mu x_i, X, \mu X_i, *$. Obvious. 

\

\noindent \textbf{Step Case}: $o_1= \lambda y.n$. We have $\Gamma \vdash \nu(\lambda y.[o_2/x]n) \equiv \lambda y.\nu([o_2/x]n) \stackrel{IH}{\Rightarrow_{\beta\mu}} \lambda y.\nu([o_2'/x]n) \equiv \nu(\lambda y.[o_2'/x]n)$.

\

\noindent \textbf{Step Case}: $o_1= n n'$. We have $\Gamma \vdash \nu([o_2/x]n [o_2/x]n') \equiv \nu([o_2/x]n) \nu([o_2/x]n')\stackrel{IH}{\Rightarrow_{\beta\mu}} \nu([o_2'/x]n) \nu([o_2'/x]n')\equiv \nu([o_2'/x]n[o_2'/x]n)$.

\

\noindent The other cases are similar.

\end{proof}

\begin{lemma}
\label{key}
If $\Gamma \vdash o_1 \Rightarrow_{\beta\mu} o_1'$ and $\Gamma \vdash o_2 \Rightarrow_{\beta\mu} o_2'$, then $\Gamma \vdash \nu([o_2/y]o_1) \Rightarrow_{\beta\mu} \nu([o_2'/y]o_1')$ and $\Gamma \vdash \nu([o_2/Y]o_1) \Rightarrow_{\beta\mu} \nu([o_2'/Y]o_1')$.
\end{lemma}

\begin{proof}

\noindent We prove this by induction on the derivation of $\Gamma \vdash o_1 \Rightarrow_{\beta\mu} o_1'$.
  
\

\noindent \textbf{Base Case:}

\

\noindent \infer{\Gamma \vdash n \Rightarrow_{\beta \mu} n}{}

\

\noindent \infer{\Gamma \vdash N \Rightarrow_{\beta \mu} N}{}

\

\noindent \infer{\Gamma \vdash K \Rightarrow_{\beta \mu} K}{}

\

\noindent By lemma \ref{lemma7}.

\

\noindent \textbf{Base Case:}

\

\noindent \infer{\Gamma \vdash \mu x_i\Rightarrow_{\beta\mu} \nu(\mu t_i)}{x_i \mapsto t_i \in \mu}

\

\noindent Since $y \notin \mathrm{FV}(\mu x_i)$ and $\mu$ is local, we have $\nu([n_2/y]\mu x_i) \equiv \nu(\mu x_i)$ and $\nu(\mu x_1) \equiv \mu x_i \Rightarrow_{\beta\mu} \nu(\mu t_i) \equiv \nu(\nu(\mu t_i))$(lemma \ref{norm:iden}). 

\

\noindent \textbf{Base Case:}

\

\infer{\Gamma \vdash  x \Rightarrow_{\beta\mu} \nu( t)}{(x \mapsto t) \in \Gamma}

\

\noindent In this case, $x$ is unsubstitutable. So this situation will not arise.

\

\noindent \textbf{Step Case:}

\

\noindent \infer{\Gamma \vdash (\lambda x.n_a) n_b \Rightarrow_{\beta\mu} \nu([n_a'/x]n_b')}{\Gamma \vdash n_a\Rightarrow_{\beta\mu} n_a' & \Gamma \vdash n_b\Rightarrow_{\beta\mu} n_b'}

\

\noindent We have $\Gamma \vdash \nu((\lambda x.[n_2/y]n_a) [n_2/y] n_b) \equiv (\lambda x.\nu([n_2/y]n_a)) \nu([n_2/y] n_b)$

$ \stackrel{IH}{\Rightarrow_{\beta\mu}} \nu([\nu([n_2'/y] n_b')/x]\nu([n_2'/y] n_a')) \equiv \nu([n_2'/y]([n_b'/x]n_a'))$. The last equality is by lemma \ref{norm:iden}. Here we first apply induction hypothesis to reduce, then apply ${\Rightarrow_{\beta\mu}}$.

\

\noindent \textbf{Step Case:}

\

\noindent \infer{\Gamma \vdash \lambda x.n \Rightarrow_{\beta\mu} \lambda x.n'}{\Gamma \vdash n \Rightarrow_{\beta\mu}n' }

\

\noindent We have $\Gamma \vdash \nu(\lambda x.[n_2/y]n) \equiv \lambda x.\nu([n_2/y]n) \stackrel{IH}{\Rightarrow_{\beta\mu}} \lambda x.\nu([n_2'/y]n') \equiv \nu(\lambda x.[n_2'/y]n') $

\

\noindent \textbf{Step Case:}

\

\noindent \infer{\Gamma \vdash n_a n_b \Rightarrow_{\beta\mu} n_a'n_b'}{ \Gamma \vdash n_a\Rightarrow_{\beta\mu} n_a' & \Gamma \vdash n_b\Rightarrow_{\beta\mu} n_b'}

\

\noindent We have $\Gamma \vdash \nu([n_2/y]n_a [n_2/y] n_b) \equiv \nu([n_2/y]n_a) \nu([n_2/y] n_b)$

$ \stackrel{IH}{\Rightarrow_{\beta\mu}} \nu([n_2'/y] n_a') \nu([n_2'/y] n_b')\equiv \nu([n_2'/y](n_a'n_b'))$.

\

\noindent The other cases are similar as above. 

\end{proof}


\begin{lemma}[Diamond Property] 
  \label{diamond}
  If $ \Gamma \vdash o \Rightarrow_{\beta\mu} o'$ and $\Gamma \vdash o \Rightarrow_{\beta\mu} o''$, then there exists $o'''$ such that $ \Gamma \vdash o'' \Rightarrow_{\beta\mu} o'''$ and $ \Gamma \vdash o' \Rightarrow_{\beta\mu} o'''$.
\end{lemma}

\begin{proof}
  \noindent By induction on the derivation of $\Gamma \vdash o \Rightarrow_{\beta\mu} o'$. 

\noindent \textbf{Base Case:}

\

\noindent \infer{\Gamma \vdash n \Rightarrow_{\beta \mu} n}{}

\

\noindent Obvious.

\

\noindent \textbf{Base Case:}

\

\noindent \infer{\Gamma \vdash x \Rightarrow_{\beta\mu} \nu( t)}{(x \mapsto t) \in \Gamma}

\

\noindent Obvious.

\

\noindent \textbf{Base Case:}

\

\noindent \infer{\Gamma \vdash \mu x_i\Rightarrow_{\beta\mu} \nu(\mu t_i)}{}

\

\noindent Obvious. 

\

\noindent \textbf{Step Case:}

\

\noindent \infer{\Gamma \vdash (\lambda x.n_1) n_2 \Rightarrow_{\beta\mu} \nu([n_2'/x]n_1')}{ \Gamma \vdash n_1\Rightarrow_{\beta\mu} n_1' &\Gamma \vdash n_2\Rightarrow_{\beta\mu} n_2'}

\

\noindent Suppose $\Gamma \vdash (\lambda x.n_1) n_2 \Rightarrow_{\beta\mu}(\lambda x.n_1'') n_2''$, where $\Gamma \vdash n_1 \Rightarrow_{\beta\mu}n_1''$ and $\Gamma \vdash n_2 \Rightarrow_{\beta\mu} n_2''$. By IH, there exist $n_1''', n_2'''$ such that $\Gamma \vdash n_1'' \Rightarrow_{\beta\mu}n_1'''$ and $\Gamma \vdash n_1' \Rightarrow_{\beta\mu}n_1'''$ and $\Gamma \vdash n_2' \Rightarrow_{\beta\mu} n_2'''$ and $\Gamma \vdash n_2' \Rightarrow_{\beta\mu}n_2'''$ . By lemma \ref{key}, $\Gamma \vdash \nu([n_1'/x]n_2') \Rightarrow_{\beta\mu} \nu([n_1'''/x]n_2''')$, also $\Gamma \vdash (\lambda x.n_1'') n_2''\Rightarrow_{\beta\mu} \nu([n_1'''/x]n_2''')$.  

\

\noindent Suppose $\Gamma \vdash (\lambda x.n_1) n_2 \Rightarrow_{\beta\mu}\nu([n_2''/x]n_1'') $, where $\Gamma \vdash n_1 \Rightarrow_{\beta\mu}n_1''$ and $\Gamma \vdash n_2 \Rightarrow_{\beta\mu} n_2''$. By IH, there exist $n_1''', n_2'''$ such that $\Gamma \vdash n_1'' \Rightarrow_{\beta\mu}n_1'''$ and $\Gamma \vdash n_1' \Rightarrow_{\beta\mu}n_1'''$ and $\Gamma \vdash n_2' \Rightarrow_{\beta\mu} n_2'''$ and $\Gamma \vdash n_2' \Rightarrow_{\beta\mu}n_2'''$ . By lemma \ref{key}, $\Gamma \vdash \nu([n_1'/x]n_2') \Rightarrow_{\beta\mu} \nu([n_1'''/x]n_2''')$ and $\Gamma \vdash \nu([n_1''/x]n_2'') \Rightarrow_{\beta\mu} \nu([n_1'''/x]n_2''')$.

\

\noindent The other cases are either similar to the one above or easy.

\end{proof}

By lemma \ref{diamond} and lemma \ref{sub}, we conclude the confluence of $\to_{\beta\mu}$.

\begin{lemma}
  $\to_{\iota}$ is confluent.
\end{lemma}
\begin{proof}
  This is obvious since $\to_{\iota}$ is deterministic. 
\end{proof}
\begin{lemma}
\label{cus}
If $\Gamma \vdash o \to_{\beta,\mu} o'$, then $\Gamma \vdash [o_1/x]o \to_{\beta,\mu} [o_1/x]o'$ and $\Gamma \vdash [o_1/X]o \to_{\beta,\mu} [o_1/X]o'$ for any $o_1$. 
\end{lemma}
\begin{proof}
  Obvious.
\end{proof}
\begin{lemma}
 $\to_{\beta,\mu}$ commutes with $\to_{\iota}$. i.e. if $\Gamma \vdash T_1 \to_{\beta,\mu} T_2$ and $\Gamma \vdash T_1 \to_{\iota} T_3$, then there exists $T_4$ such that $\Gamma \vdash T_2 \to_{\iota} T_4$ and $\Gamma \vdash T_3 \to_{\beta,\mu} T_4$. 
\end{lemma}
\begin{proof}
  Since $\Gamma \vdash T_1 \to_{\iota} T_3$, we know that $T_1 \equiv \iota x.T'$ and $T_3 \equiv [t/x]T'$. We also have $\Gamma \vdash T_1\equiv \iota x.T' \to_{\beta,\mu} T_2$. By inversion,
we know that $T_2 \equiv \iota x.T''$ with $\Gamma \vdash T' \to_{\beta,\mu} T''$. By lemma \ref{cus}, we know that 
$\Gamma \vdash [t/x]T' \to_{\beta,\mu} [t/x]T''$. Thus $T_4 \equiv [t/x]T''$ and $\Gamma \vdash \iota x.T'' \to_{\iota} [t/x]T''$.
\end{proof}

\begin{lemma}
\label{subo}
  If $\Gamma \vdash o_1 \to_o o_2$, then $\Gamma \vdash [o/x]o_1 \to_o [o/x]o_2$ and $\Gamma \vdash [o/X]o_1 \to_o [o/X]o_2$.
\end{lemma}
\begin{proof}
By induction on derivaton. 
\end{proof}

\begin{lemma}
\label{subo2}
  If $\Gamma \vdash o_1 \to_o o_2$, then $\Gamma \vdash [o_1/x]o \hookrightarrow_o [o_2/x]o$
  and $\Gamma \vdash [o_1/X]o \hookrightarrow_o [o_2/X]o$.
\end{lemma}
\begin{proof}
  By induction on the structure of $o$. 
\end{proof}


\begin{lemma}
  $\to_o$ has diamond property, thus is confluent.
\end{lemma}
\begin{proof}
  Straightforward induction.
\end{proof}

\begin{lemma}
  $\to_o$ commutes with $\to_{\iota}$. 
\end{lemma}
\begin{proof}
  Suppose $\Gamma \vdash \iota x.T'\to_{\iota} [t/x]T'$ and $\Gamma \vdash \iota x.T' \to_o \iota x.T''$ with $\Gamma \vdash T' \to_o T''$. Then by lemma \ref{subo}, we have $\Gamma \vdash [t/x]T' \to_o [t/x]T''$. We also have $\Gamma \vdash \iota x.T'' \to_{\iota} [t/x]T''$. 
\end{proof}

\begin{lemma}
  $\to_o$ weak commutes with $\to_{\beta}$. 
\end{lemma}
\begin{proof}
\noindent By induction on $\to_o$.

\

\noindent \textbf{Case}: $\Gamma \vdash \mu t \to_o t$, where $\mu \in \Gamma$.

\

\noindent If $\Gamma \vdash \mu x_i \to_{\beta} \mu t_i$, where $x_i \mapsto t_i \in \mu$, then
$\Gamma \vdash \mu x_i \to_o x_i$. So we have $\Gamma \vdash \mu t_i \to_o t_i$ and $\Gamma \vdash x_i \to_{\beta} t_i$ since $\mu \in \Gamma$. 

\

\noindent If $\Gamma \vdash \mu t \to_{\beta} \mu t'$, with $\Gamma \vdash t \to_{\beta} t'$. So we have $\Gamma \vdash t \to_{\beta} t'$ and $\Gamma \vdash \mu t' \to_o t'$. 

\

\noindent \textbf{Case}: $\Gamma \vdash (\lambda x.t_1)t_2 \to_o (\lambda x.t_1')t_2$, where 
$\Gamma \vdash t_1 \to_o t_1'$. 

\

\noindent Suppose $\Gamma \vdash (\lambda x.t_1)t_2 \to_{\beta} [t_2/x]t_1$. By lemma \ref{subo}, we know that $\Gamma \vdash [t_2/x]t_1 \to_o [t_2/x]t_1'$. And we also have $\Gamma \vdash (\lambda x.t_1')t_2 \to_{\beta} [t_2/x]t_1'$. 

\

\noindent \textbf{Case}: $\Gamma \vdash (\lambda x.t_1)t_2 \to_o (\lambda x.t_1)t_2'$, where 
$\Gamma \vdash t_2 \to_o t_2'$. 

\

\noindent Suppose $\Gamma \vdash (\lambda x.t_1)t_2 \to_{\beta} [t_2/x]t_1$. By lemma \ref{subo2}, we know that $\Gamma \vdash [t_2/x]t_1 \hookrightarrow_o [t_2'/x]t_1$. And we also have $\Gamma \vdash (\lambda x.t_1)t_2' \to_{\beta} [t_2'/x]t_1$. 

\

\noindent The other cases are similar.
\end{proof}

\begin{lemma}
$\to_o$ weak commutes with $\to_{\mu}$. i.e. if $\Gamma \vdash o \to_{o} o'$ and $\Gamma \vdash o \to_{\mu} o''$, then there exists a $o_1$ such that $\Gamma \vdash o'' \to_{o}^* o_1$ and $\Gamma \vdash o' \hookrightarrow_{\mu} o_1$.

\end{lemma}

\begin{proof}
\noindent  By induction on $\Gamma \vdash o \to_{o} o'$. 

\

\noindent \textbf{Case}: $\Gamma \vdash \mu t \to_o t$, where $\mu \in \Gamma$.

\

\noindent Suppose $\Gamma \vdash \mu t \to_{\mu} t$ with $\mathrm{dom}(\mu) \# \mathrm{FV}(t)$. This case
is obvious. 

\

\noindent Suppose $t \equiv \lambda x.t_2$ and $\Gamma \vdash \mu (\lambda x.t_2) \to_{\mu} \lambda x.\mu t_2$. Then $\Gamma \vdash \lambda x.t_2 \hookrightarrow_{\mu} \lambda x.t_2$ and $\Gamma \vdash \lambda x.\mu t_2 \to_o \lambda x.t_2$.   

\

\noindent Suppose $t \equiv t_2 t_3$ and $\Gamma \vdash \mu (t_2 t_3) \to_{\mu} (\mu t_2)(\mu t_3)$. Then $\Gamma \vdash t_2 t_3 \hookrightarrow_{\mu} t_2 t_3$ and $\Gamma \vdash (\mu t_2)(\mu t_3) \to_o^* t_2 t_3$.

\

\noindent The other cases are similar.   
\end{proof}


\section{Proofs for Section \ref{result}}
\label{pres}
\begin{lemma}
\label{type}
  Let $([\Gamma, \Delta], T_1) {\to_{o,\iota,\beta,\mu,i,g,I,G}}^* ([\Gamma], T_2)$. If $\Gamma, \Delta \vdash t:T_1$ with $\mathrm{dom}(\Delta) \# \mathrm{FV}(t)$, then $\Gamma \vdash t:T_2$. 
\end{lemma}

\noindent \textbf{Note}: We write $\stackrel{t}{\to}_{\beta,\mu,\iota,o, i, g, I, G}$ to mean
the same thing as ${\to}_{\beta,\mu,\iota,o, i, g, I, G}^*$ with an emphasis on the subject $t$. 

\begin{lemma} 
\label{conv}
 If $([\Gamma], T_1) \stackrel{t}{\to}_{\beta,\mu,\iota,o, i, g, I, G} ([\Gamma'],T_2)$ and $\Gamma \vdash t =_{\beta,\mu} t'$, then $([\Gamma], T_1) \stackrel{t'}{\to}_{\beta,\mu,\iota,o, i, g, I, G} ([\Gamma'],T_2)$.  
\end{lemma} 
\begin{proof} By induction on the length of $([\Gamma],T_1) \stackrel{t}{\to}_{\beta,\mu,\iota,o, i,g, I, G} ([\Gamma],T_2)$. Note that this lemma is \textbf{not} subject expansion, do not get confused.
\end{proof}


\begin{lemma} 
    \label{perm} If $\Gamma, \tilde{\mu}, y:T'
\vdash t:T$ , then $\Gamma, y: \mu  T',\tilde{\mu} 
 \vdash t :T$.  
 \end{lemma}
\begin{proof} By induction on the
derivation of $\Gamma, \tilde{\mu} , y:T' \vdash t:T$.
\end{proof}

\noindent \textbf{Note}: If $\Delta = x:T,..., X:\kappa$, then $\mu \Delta := x:\mu T,..., X:\mu \kappa$. 

\begin{lemma} 
    \label{metacong} 
        If $([\Gamma, \tilde{\mu}, \Delta], T) \stackrel{t}{\to}_{\beta,\mu,\iota,o, i, g, I, G} ([\Gamma, \tilde{\mu}, \Delta'], T')$ for some $\Delta, \Delta'$ and $\Gamma, \mu \Delta , \tilde{\mu}
\vdash \mathsf{ok}$, then $([\Gamma, \mu \Delta], \mu T) \stackrel{\mu t }{\to}_{\beta,\mu,\iota,o, i, g, I, G} ([\Gamma, \mu \Delta'], \mu T')$.
 \end{lemma} 
 \begin{proof} By induction on the length of $([\Gamma, \tilde{\mu}, \Delta], T) \stackrel{t}{\to}_{\beta,\mu,\iota,o, i, g, I, G} ([\Gamma, \tilde{\mu}, \Delta'], T')$. We list a few cases.

\

\noindent\textbf{Case}: $([\Gamma, \tilde{\mu}, \Delta],T) {=_{\beta,\mu, o}} ([\Gamma, \tilde{\mu}, \Delta],T')$.

\

\noindent Use lemma \ref{perm}, we have $([\Gamma, \mu \Delta], \mu T)   =_{\beta,\mu,o}  ([\Gamma , \mu \Delta'], \mu T')$. 

\

\noindent\textbf{Case}: $([\Gamma, \tilde{\mu}, \Delta], \iota x.T) {=_{\iota}} ([\Gamma, \tilde{\mu}, \Delta], [t/x]T)$. 

\

\noindent We know $([\Gamma, \mu \Delta] , \mu \iota x.T ) {=_{\mu}} ( [\Gamma, \mu \Delta],\iota x.\mu T)  {=_{\iota}}([\Gamma, \mu \Delta], [\mu t/x] \mu T) {=_{\mu}} ([\Gamma, \mu \Delta], \mu [t/x]T)$.

\

\noindent\textbf{Case}: $([\Gamma, \tilde{\mu}, \Delta], \Delta X:\kappa.T) {\to_{i}} ([\Gamma, \tilde{\mu}, \Delta],[T'/X]T)$ with $\Gamma, \tilde{\mu}, \Delta \vdash T':\kappa$.

\

\noindent We know $([\Gamma, \mu \Delta], \mu (\Delta X:\kappa.T)) {=_{\mu}} ([\Gamma, \mu \Delta], \Delta X:\mu \kappa.\mu T)  {\to_{i}} ([\Gamma, \mu \Delta],[\mu T'/X] \mu T) {=_{\mu}} ([\Gamma, \mu \Delta], \mu ([T'/X]T))$ with $\Gamma, \mu\Delta \vdash \mu T': \mu \kappa$.

\

\noindent\textbf{Case}: $([\Gamma, \tilde{\mu}, \Delta, X:\kappa],T) {\to_{g}} ([\Gamma, \tilde{\mu}, \Delta],\Delta X:\kappa.T)$ with $\Gamma, \tilde{\mu},\Delta \vdash \kappa:\Box$.

\

\noindent We know $([\Gamma, \mu \Delta, X: \mu \kappa],\mu T)  {\to_{g}} ([\Gamma, \mu\Delta], \Delta X:\mu \kappa. \mu T) {=_{\mu}} ([\Gamma, \mu\Delta], \mu (\Delta X:\kappa.T))$ with $\Gamma, \mu\Delta \vdash \mu \kappa:\Box$.

\

\noindent\textbf{Case}: $([\Gamma, \tilde{\mu}, \Delta], \forall x:T'.T) {\to_{I}} ([\Gamma, \tilde{\mu}, \Delta], [t/x]T)$ with $\Gamma, \tilde{\mu}, \Delta \vdash t:T'$.

\

\noindent We know $([\Gamma, \mu \Delta],\mu(\forall x:T'.T)) {=_{\mu}} ([\Gamma, \mu \Delta], \forall x:\mu T'.\mu T)  {\to_{I}} ([\Gamma, \mu \Delta],[\mu t/x] \mu T) {=_{\mu}}([\Gamma, \mu \Delta], \mu [t/x]T)$ with $\Gamma,\mu\Delta \vdash \mu t: \mu T'$.

\

\noindent\textbf{Case}: $([\Gamma, \tilde{\mu}, \Delta, x:T'], T) {\to_{G}} ([\Gamma, \tilde{\mu}, \Delta], \forall x:T'.T)$ with $\Gamma, \tilde{\mu}, \Delta \vdash T':*$.

\

\noindent We know $([\Gamma, \mu \Delta, x:\mu T'],\mu T)  {\to_{G}}([\Gamma, \mu \Delta], \forall x:\mu T'. \mu T) {=_{\mu}} ([\Gamma, \mu \Delta],\mu (\forall x:T'.T))$ with $\Gamma, \mu \Delta \vdash \mu T':*$.


\end{proof}

\begin{lemma}[Inversion I]
If $\Gamma \vdash x:T$, then exist $\Delta, T_1$ such that $([\Gamma, \Delta], T_1) {\to_{o,\iota,\beta,\mu,i,g,I,G}^*} ([\Gamma], T)$ and $(x:T_1) \in \Gamma$.
\end{lemma}

\begin{lemma}[Inversion II]
If $\Gamma \vdash t_1 t_2:T$, then exist $\Delta, T_1, T_2$ such that $\Gamma, \Delta \vdash t_1:\Pi x:T_1.T_2$ and $\Gamma, \Delta \vdash t_2:T_1$ and $([\Gamma, \Delta], [t_2/x]T_2) {\to_{o,\iota,\beta,\mu,i,g,I,G}^*} ([\Gamma],T)$. 
\end{lemma}

\begin{lemma}[Inversion III]
If $\Gamma \vdash \lambda x.t:T$, then exist $\Delta, T_1, T_2$ such that $\Gamma, \Delta , x:T_1 \vdash t:T_2$ and $([\Gamma, \Delta], \Pi x:T_1. T_2) {\to_{o,\iota,\beta,\mu,i,g,I,G}^*} ([\Gamma], T)$. 
\end{lemma}

\begin{lemma}[Inversion IV]
If $\Gamma \vdash \mu t:T$, then exist $\Delta, T_1$ such that $\Gamma, \Delta, \tilde{\mu} \vdash t:T_1$ and $([\Gamma, \Delta], \mu T_1) {\to_{o,\iota,\beta,\mu,i,g,I,G}^*} ([\Gamma],T)$.
\end{lemma}


\begin{lemma}[Substitution]
\label{subst}
\

  \begin{enumerate}
  \item   If $\Gamma \vdash t:T$, then for any mixed substitution $\phi$ with $\mathrm{dom}(\phi) \# \mathrm{FV}(t) $, $\phi \Gamma \vdash t: \phi T$.
\item If $\Gamma, x:T \vdash t:T'$ and $\Gamma \vdash t':T$, then $\Gamma \vdash [t'/x]t:[t'/x]T'$.
  \end{enumerate}

\end{lemma}

\begin{proof}
  By induction on derivation.
\end{proof}

\begin{theorem}
  If $\Gamma \vdash t:T$ and $\Gamma \vdash t \to_{\beta, \mu} t'$ and $\Gamma \vdash \mathsf{wf}$, then $\Gamma \vdash t':T$.
\end{theorem}
\begin{proof}
  By induction on derivation of $\Gamma \vdash t:T$. We list a few interesting 
cases.

\

\noindent \textbf{Case:}

\

\infer{\Gamma \vdash x:T}{ x:T \in \Gamma}

\

\noindent If $\Gamma \vdash x \to_{\beta} t'$, this means $ (x:T) \mapsto t'
\in \Gamma$ and $\Gamma \vdash t':T$ since $\Gamma \vdash \mathsf{wf}$.

\

\noindent \textbf{Case}:

\

\infer[\textit{App}]{\Gamma \vdash t t':[t'/x]T_2}{\Gamma
\vdash t:\Pi x:T_1.T_2 & \Gamma \vdash t': T_1}

\

\noindent Suppose $\Gamma \vdash (\lambda x.t_1) t_2 \to_{\beta} [t_2/x]t_1$. We know that
$\Gamma \vdash \lambda x.t_1 : \Pi x:T_1. T_2$ and $\Gamma \vdash t_2:T_1$. By
inversion on $\Gamma \vdash \lambda x.t_1 : \Pi x:T_1. T_2$, we know that 
there exist $\Delta, T_1', T_2'$ such that $\Gamma, \Delta, x:T_1' \vdash t_1:T_2'$
and $([\Gamma, \Delta], \Pi x:T_1'.T_2') {\to_{o,\iota,\beta,\mu,i,g,I,G}^*} ([\Gamma], \Pi x:T_1.T_2)$. 
By Theorem \ref{comp}, we have $([\Gamma, \Delta], \phi(\Pi x:T_1'.T_2')) =_{o,\iota,\beta,\mu} ([\Gamma, \Delta],\Pi x:T_1. T_2)$. By Church-Rosser
of $=_{o,\iota,\beta,\mu}$, we have $\Gamma, \Delta \vdash \phi T_1'=_{o,\beta,\mu}  T_1$ and $\Gamma, \Delta \vdash \phi T_2' =_{o,\beta,\mu} T_2$. 
So by (1) of lemma \ref{subst}, we have $\Gamma,\phi(\Delta), x:\phi T_1' \vdash t_1: \phi T_2'$ with $\mathrm{dom}(\phi(\Delta)) \# (\mathrm{FV}(\phi T_1') \cup \mathrm{FV}(\phi T_2') \cup \mathrm{FV}(t_1)) $. So $\Gamma,\phi(\Delta), x: T_1 \vdash t_1: T_2$. Since $\Gamma \vdash t_2:T_1$, by (2) of lemma \ref{subst}, $\Gamma, \phi(\Delta) \vdash [t_2/x]t_1: [t_2/x]T_2$. So we have $\Gamma\vdash [t_2/x]t_1: [t_2/x]T_2$. 

\

\noindent \textbf{Case:}

\

\infer{\Gamma \vdash \mu t: \mu T}{\Gamma, \tilde{\mu}
\vdash t:T &  \Gamma, \tilde{\mu} \vdash \mathsf{ok} }

\

\noindent Suppose  $\Gamma \vdash \mu x_j \to_{\beta} \mu
t_j$, where $x_j \mapsto t_j \in \mu$. We have $\Gamma, \tilde{\mu} \vdash x_j:T$. By
inversion, $\Gamma, \tilde{\mu}, \Delta \vdash x_j:T_j$ and $([\Gamma, \tilde{\mu}, \Delta], T_j) \stackrel{x_j}{\to}_{\beta,\mu,\iota,o, i,g,I,G}  ([\Gamma, \tilde{\mu}], T)$. 
 Since $\Gamma, \tilde{\mu}, \Delta \vdash x_j =_{\beta} t_j$ and by lemma \ref{conv}, we   
get $([\Gamma, \tilde{\mu} , \Delta],T_j) \stackrel{t_j}{\to}_{\beta,\mu,\iota,o, i, g, I, G} ([\Gamma, \tilde{\mu}],T)$. 
Since $\Gamma, \tilde{\mu}, \Delta \vdash  t_j : T_j$, by lemma \ref{type}, $\Gamma, \tilde{\mu}\vdash t_j:T$. Thus we have $\Gamma \vdash \mu t_j : \mu T$.

\

\noindent Suppose  $\Gamma\vdash \mu t \to_{\mu} t$, where $\mathsf{FV}(t) \# \mathrm{dom}(\mu)$. 
We have $\Gamma, \tilde{\mu} \vdash t : T$ and $(\mathrm{FV}(t)\cup \mathrm{FV}(T)) \# \mathrm{dom} (\mu)$. So we have $([\Gamma],\mu T)  {=}_{\mu} ([\Gamma], T)$. We also know that $\Gamma \vdash t : T$, so $\Gamma
\vdash t : \mu T$(lemma \ref{type}).

\

\noindent Suppose $\Gamma\vdash \mu \lambda x.t \to_{\mu} \lambda  x. \mu  t$. We have $\Gamma, \tilde{\mu} \vdash \lambda  x.t : T$ and 
$\Gamma, \tilde{\mu}, \Delta, x:T_1 \vdash t : T_2$ and $([\Gamma, \tilde{\mu}, \Delta],
\Pi  x:T_1.T_2) \stackrel{\lambda  x.t}{\to}_{\beta,\mu,\iota,o, i,g, I, G}  ([\Gamma, \tilde{\mu}],T)$(by inversion). Thus we have $\Gamma, \mu \Delta, x:\mu T_1 \vdash \mu
  t: \mu   T_2$(lemma \ref{perm}) and
$([\Gamma, \mu \Delta], \mu(\Pi  x:T_1.T_2)) \stackrel{\mu
 \lambda  x.t}{\to}_{\beta,\mu,\iota,o, i,g, I, G} ([\Gamma], \mu  T)$(lemma \ref{metacong}). By lemma \ref{conv}, $([\Gamma, \mu \Delta], (\Pi  x:\mu  T_1.\mu  T_2))
\stackrel{\lambda  x.\mu  t}{\to}_{\beta,\mu,\iota,o, i, g, I, G} ([\Gamma], \mu  T)$. 
Also, $\Gamma, \mu \Delta \vdash \lambda  x.\mu t : \Pi  x: (\mu  T_1).(\mu T_2)$.  
So by lemma \ref{type}, $\Gamma \vdash \lambda x.\mu   t :  \mu  T$.

\

\noindent Suppose $\Gamma\vdash \mu  (t_1' t_2') \to_{\mu} (\mu  t_1')( \mu  t_2')$. We have $\Gamma, \tilde{\mu} \vdash t_1't_2' : T $ and $\Gamma, \tilde{\mu}, \Delta \vdash t_1' : \Pi  x:T_1. T_2$ and $\Gamma, \tilde{\mu}, \Delta \vdash t_2' : T_1$ and $([\Gamma, \tilde{\mu}, \Delta], [t_2'/x]T_2) \stackrel{t_1't_2'}{\to}_{\beta,\mu,\iota,o, i, g, I, G} ([\Gamma, \tilde{\mu}], T)$(by inversion). Thus we have $\Gamma , \mu \Delta \vdash \mu   t_1':  \mu  (\Pi x:T_1.T_2)$ and $\Gamma, \mu \Delta \vdash \mu   t_2':  \mu T_1$ and $([\Gamma, \mu \Delta], \mu ([t_2'/x]T_2)) \stackrel{\mu  (t_1' t_2')}{\to}_{\beta,\mu,\iota,o, i, g, I, G} ([\Gamma],\mu T) $(lemma \ref{metacong}). By
lemma \ref{conv}, we have $([\Gamma, \mu \Delta], \mu ([t_2'/x]T_2)) \stackrel{(\mu t_1')(\mu t_2')}{\to}_{\beta,\mu,\iota,o, i, g, I, G} ([\Gamma],\mu T) $. So $\Gamma, \mu \Delta \vdash
(\mu   t_1')(\mu   t_2') :[\mu t_2'/x]\mu  T_2$ and then $\Gamma \vdash (\mu   t_1')(\mu   t_2') : \mu T$(lemma \ref{type}).

\end{proof}

%% Impossible to understand if we device an annotated language. But, why not, 
%% it is already impossible to understand.

%% \section{An Annotated Language for $\self$}
%% \label{ann}
%% \begin{definition}[Annotated Terms and Types]

%% \noindent Terms  $t ::= \ x \ | \ \lambda x:T.t \ | \ t t' \ | \ t [t'] \ | \ [\lambda x:T].t \ | \ t [p] | \ \mu t \ | \ \uparrow t \ | \ \downarrow t$

%% \noindent Joinability $p ::= \ \mathsf{join}$
  
%% \noindent  \textit{Types} $T \ ::= $

%% \noindent $\ X \ | \ \Pi X:\kappa.T \ | \ \Pi x:T_1.T_2 \ | \ \forall x:T_1.T_2 \ | \ \iota x.T \ | \ T \ t \ | \ \lambda X:\kappa.T \ | \ \lambda x:T'.T\ | \ T_1 T_2 \ | \ \mu T \ | \ T[p]$

%% \noindent \textit{Kinds} $\kappa \ ::= \ * \ | \ \Pi x:T.\kappa \ | \  \Pi X:\kappa'. \kappa \  | \ \mu \kappa$ 

%% \noindent \textit{Context} $\Gamma \ :: = \ \cdot \ | \ \Gamma, x:T \ |  \ \Gamma, X:\kappa\ | \ \Gamma, \tilde{\mu}$

%% \noindent \textit{Closure} $\mu \ ::= \ \Mb{x}{t}{N}{T} \cup \Mb{X}{T}{M}{\kappa}$

%% \end{definition}

    
%% \noindent $\Gamma, \mu \vdash \mathsf{ok}$ stands for $\{\Gamma, \mu \vdash t_j: T_j\}_{(t_j:T_j) \in \mu}$ and $\{\Gamma, \mu \vdash T_j: \kappa_j\}_{(T_j:\kappa_j) \in \mu}$. Now let us see how to erase annotated terms and type to the unannotated ones. 

%% \begin{definition}[Annotation Erasure on Terms]
%% \

%% \begin{tabular}{lll}
%%  $| x| := x$
%%  &  
%%  $|\lambda x:T.t| := \lambda x.t $
 
%%  &
%%  $|t t'| := |t| \ |t'| $
 
%%     \\
    
%% $|t [t'] |:= |t| $
    
%%     &
    
%%     $|[\lambda x:T].t| := |t| $
    
%%     &
%%     $ | t [p] | := |t| $
%%     \\
    
%%     $ |\mu t | := |\mu| \ |t| $
    
%%     &
    
%%     $ | \uparrow t| := |t| $
    
%%     &
%%     $| \downarrow t| := |t|$
%%     \\
%%     $|x:t \mapsto t', \mu| := x\mapsto t', |\mu|$
    
%%   \end{tabular}
%% \end{definition}

%% \begin{definition}[Annotation Erasure for Types]
%% \

%% \begin{tabular}{lll}
%%   $| \lambda X:\kappa.T| := \lambda X.|T|$ 
%%     &
%%    $|\lambda x:T'.T| := \lambda x.|T| $
    
%%     &
    
%%     $ |T[p]| := |T|$
%%   \\
  
%%   $|X| := X$
  
%%   & $| \Pi x:T_1.T_2| := \Pi x:|T_1|. |T_2| $
  
%%   & $|\forall x:T_1.T_2| := \forall x:|T_1|. |T_2|$
%%   \\
  
%%   $ |\iota x.T|:= \iota x.|T|$
  
%%   &
%%   $ |T \ t | := |T|\ |t| $
  
%%   & $ | T_1 T_2 | := |T_1| \ |T_2| $
  
%%   \\
%%   $ |\mu T | := |\mu|\ |T|$

%%   \end{tabular}

%% \end{definition}

%% \begin{theorem}[Soundness]
%%   If in the annotated language, $\Gamma \vdash t:T$, then $|\Gamma| \vdash |t| : |T|$ in 
%%   the unannotated language (we assume for $\mu \in \Gamma$, $|\mu| = \mu$.).
%% \end{theorem}


%% \begin{figure}
%% \begin{center}
%% \footnotesize{
%% \begin{tabular}{ll}
%% \infer{\Gamma \vdash X:\kappa}{(X:\kappa) \in \Gamma}

%% &
%% \infer{\Gamma \vdash T[p]  : \kappa'}{\Gamma \vdash T:
%% \kappa & \Gamma \vdash p: \kappa \cong \kappa' & \Gamma \vdash \kappa': \Box}

%% \\
%% \\
%% \infer{\Gamma \vdash \Pi x:T_1.T_2 : *}{ \Gamma \vdash T_1 : * &
%% \Gamma, x: T_1 \vdash T_2 : *}

%% &


%% \infer{\Gamma \vdash \Pi X:\kappa. T : *}{ \Gamma, X:\kappa \vdash T : * & \Gamma \vdash \kappa:\Box}

%% \\
%% \\

%% \infer{\Gamma \vdash \mu T: \mu \kappa}{\Gamma, \mu
%% \vdash T:\kappa & \Gamma, \mu \vdash \mathsf{ok}}

%% &

%% \infer[\textit{Self}]{\Gamma \vdash \iota x.T : *}{\Gamma, x:\iota x.T \vdash T : *}
%% \\
%% \\

%% \infer{\Gamma \vdash \lambda X:\kappa.T: \Pi X:\kappa. \kappa'}{\Gamma, X:\kappa \vdash T : \kappa' & \Gamma \vdash \kappa : \Box }

%% &

%% \infer{\Gamma \vdash \lambda x:T'.T: \xi x:T'.\kappa}{\Gamma, x:T' \vdash T : \kappa & \Gamma \vdash T':*}

%% \\
%% \\
%% \infer{\Gamma \vdash S t: [t/x]\kappa}{\Gamma \vdash S: \xi x:T.\kappa & 
%% \Gamma \vdash t:T}

%% &

%% \infer{\Gamma \vdash S T: [T/X]\kappa}{\Gamma \vdash S: \Pi X:\kappa'.\kappa & 
%% \Gamma \vdash T:\kappa'}

%% \\
%% \\

%% \infer{\Gamma \vdash \forall x:T_1.T_2 : *}{ \Gamma, x:T_1 \vdash T_2 : * &
%% \Gamma \vdash T_1 : *}

%% \end{tabular}
%% }

%% \end{center}
%%       \caption{Kinding \fbox{$\Gamma \vdash T : \kappa$}}      
%%     \end{figure}

%%     \begin{figure}
%% \begin{center}
%% \footnotesize{
%% \begin{tabular}{ll}

%% \infer[\textit{Conv}]{\Gamma \vdash  t [p] : T_2}{\Gamma \vdash t:
%% T_1 & \Gamma \vdash p: T_1 \cong T_2 & \Gamma \vdash T_2:*}
%% &
%% \infer[\textit{Var}]{\Gamma \vdash x:T}{(x:T) \in \Gamma}

%% \\

%% \\

%% \infer[\textit{SelfGen}]{\Gamma \vdash \uparrow t : \iota x.T}{\Gamma
%% \vdash t: [t/x]T & \Gamma \vdash \iota x.T: * }

%% &


%% \infer[\textit{SelfInst}]{\Gamma \vdash \downarrow t: [\downarrow t/x]T}{\Gamma
%% \vdash t : \iota x.T}

%% \\
%% \\

%% \infer[\textit{Indx}]{\Gamma \vdash [\lambda x:T_1].t : \forall x:T_1.T_2}
%% {\Gamma, x:T_1 \vdash t: T_2 & \Gamma \vdash T_1:* & x \notin \mathrm{FV}(t)}

%% &

%% \infer[\textit{Dex}]{\Gamma \vdash t[t'] :[t'/x]T_2}{\Gamma
%% \vdash t: \forall x:T_1.T_2 & \Gamma \vdash t': T_1}

%% \\
%% \\

%% \infer[\textit{Mu}]{\Gamma \vdash {\mu} t: \mu T}{\Gamma, \tilde{\mu}
%% \vdash t:T &  \Gamma, \mu \vdash \mathsf{ok}}
%% &

%% \infer[\textit{Poly}]{\Gamma \vdash  \lambda X:\kappa.t :\Pi X:\kappa.T}
%% {\Gamma, X:\kappa \vdash t: T & \Gamma \vdash \kappa:\Box}

%% \\
%% \\
%% \infer[\textit{Inst}]{\Gamma \vdash t\ T':[T'/X]T}{\Gamma \vdash t: \Pi X:\kappa.T 
%% & \Gamma \vdash T': \kappa}

%% &

%% \infer[\textit{Func}]{\Gamma \vdash \lambda x:T_1.t : \Pi x:T_1. T_2}
%% {\Gamma, x:T_1 \vdash t: T_2 & \Gamma \vdash T_1:*}

%% \\
%% \\
%% \infer[\textit{App}]{\Gamma \vdash t t':[t'/x]T_2}{\Gamma
%% \vdash t: \Pi x:T_1. T_2 & \Gamma \vdash t': T_1}

%% \end{tabular}
%% }
%% \end{center}
      
%%       \caption{Annotated Typing \fbox{$\Gamma \vdash t : T$}}
      
%%     \end{figure}

\end{document}
